Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

editor-plugins: add hashbang line highlighting #1535

Merged
merged 1 commit into from
Oct 21, 2024

Conversation

lucab
Copy link
Contributor

@lucab lucab commented Oct 20, 2024

This adds supports for highlighting an hashbang line as a comment, in vscode and in highlight.js.

  • Tests added for any new code
  • Documentation added for any new functionality
  • Entries added to the respective CHANGELOG.md for any new functionality
  • Feature table on README.md updated for any listed functionality

This adds supports for highlighting an hashbang line as a comment, in
vscode and in highlight.js.
Copy link
Collaborator

@bugarela bugarela left a comment

Choose a reason for hiding this comment

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

@bugarela bugarela merged commit d2f00a0 into informalsystems:main Oct 21, 2024
14 checks passed
@lucab lucab deleted the ups/syntaxes-hashbang branch October 21, 2024 13:53
@lucab
Copy link
Contributor Author

lucab commented Oct 21, 2024

I didn't touch Vim and Emacs here. I'm not very familiar with their grammars definition, but for both I didn't see any quick way to anchor the #! to the beginning of a line. I'm leaving that up for anybody with better knowledge on those.

@bugarela
Copy link
Collaborator

I didn't touch Vim and Emacs here. I'm not very familiar with their grammars definition, but for both I didn't see any quick way to anchor the #! to the beginning of a line. I'm leaving that up for anybody with better knowledge on those.

Sure! I also don't really know how to do that, so I'll look it up some other time. VSCode is, by far, the most used one, so it's great that you fixed it there.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants