Skip to content

fix: use unicode rather than emoji#416

Merged
djsauble merged 2 commits intomainfrom
unicode
Apr 6, 2026
Merged

fix: use unicode rather than emoji#416
djsauble merged 2 commits intomainfrom
unicode

Conversation

@mkenigs
Copy link
Copy Markdown
Contributor

@mkenigs mkenigs commented Feb 17, 2026

Flox started using unicode characters instead of emoji in
flox/flox@bb5480c

@github-actions github-actions Bot added the documentation Improvements or additions to documentation label Feb 17, 2026
@github-actions
Copy link
Copy Markdown


```{ .sh }
$ flox push
Updates to myenv successfully pushed to FloxHub
Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(unrelated line)
This was completely Clauded. I didn't check spaces throughout


```{ .sh }
$ flox push
Updates to myenv successfully pushed to FloxHub
Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(unrelated line)
These aren't colorized when rendered - I'm not sure if there's an easy way to do that

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There's not, really. You'd have to figure out how to wrap these specific characters in different HTML tags and then write custom CSS for them.

@zmitchell zmitchell enabled auto-merge (rebase) March 6, 2026 17:13
@djsauble djsauble self-requested a review April 2, 2026 17:20
@djsauble djsauble self-assigned this Apr 2, 2026
@github-actions
Copy link
Copy Markdown

github-actions Bot commented Apr 6, 2026

@djsauble djsauble disabled auto-merge April 6, 2026 23:22
Flox started using unicode characters instead of emoji in
flox/flox@bb5480c
@djsauble djsauble enabled auto-merge April 6, 2026 23:26
@github-actions
Copy link
Copy Markdown

github-actions Bot commented Apr 6, 2026

@djsauble djsauble added this pull request to the merge queue Apr 6, 2026
Merged via the queue into main with commit 5477aab Apr 6, 2026
3 checks passed
@djsauble djsauble deleted the unicode branch April 6, 2026 23:31
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

documentation Improvements or additions to documentation

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants