diff options
| author | SECtim <42440411+SECtim@users.noreply.github.com> | 2021-04-06 14:54:45 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-06 14:54:45 +0200 |
| commit | 0f4409637b6d66a2746cc897ad8809e716f44121 (patch) | |
| tree | 62066a1ef5b120f580230d49425b1d131579977f /pygments/lexers/ml.py | |
| parent | 1417210b1a4d64d6c761605cff07b63b24397282 (diff) | |
| download | pygments-git-0f4409637b6d66a2746cc897ad8809e716f44121.tar.gz | |
Allow C-style line comments to start anywhere
F* actually allows for C-style `//` line comments to start anywhere in a line, not just at the beginning.
Diffstat (limited to 'pygments/lexers/ml.py')
| -rw-r--r-- | pygments/lexers/ml.py | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pygments/lexers/ml.py b/pygments/lexers/ml.py index 4709407d..a45a103e 100644 --- a/pygments/lexers/ml.py +++ b/pygments/lexers/ml.py @@ -908,7 +908,7 @@ class FStarLexer(RegexLexer): (r'\b([A-Z][\w\']*)(?=\s*\.)', Name.Namespace, 'dotted'), (r'\b([A-Z][\w\']*)', Name.Class), (r'\(\*(?![)])', Comment, 'comment'), - (r'^\/\/.+$', Comment), + (r'\/\/.+$', Comment), (r'\b(%s)\b' % '|'.join(keywords), Keyword), (r'\b(%s)\b' % '|'.join(assume_keywords), Name.Exception), (r'\b(%s)\b' % '|'.join(decl_keywords), Keyword.Declaration), |