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

fix: correct comment syntax entry #29

Merged
merged 1 commit into from
May 14, 2024

Conversation

marsam
Copy link
Contributor

@marsam marsam commented May 12, 2024

This was a mistakenly introduced by 3e496e8, adding the "2" flag into the comment syntax entry, caused to Emacs consider the // operator as a comment sequence:

    {
      foo = "foo";
    } // {
      bar = "bar";    # ← comment sequence
    }

This was a mistakenly introduced by 3e496e8, adding the "2" flag into
the comment syntax entry, caused to Emacs consider the `//` operator as
a comment sequence:

    {
      foo = "foo";
    } // {
      bar = "bar";    # ← comment sequence
    }
Copy link
Member

@purcell purcell left a comment

Choose a reason for hiding this comment

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

Thanks!

@purcell
Copy link
Member

purcell commented May 13, 2024

Unsure why I'm not getting shown the option to merge this. Just seeing:
Screenshot 2024-05-13 at 11 09 28

@Atemu
Copy link

Atemu commented May 13, 2024

You do not appear to have write access to this repository.

@purcell
Copy link
Member

purcell commented May 13, 2024

Huh, okay. An oversight, @remi-gelinas ?

@remi-gelinas
Copy link
Collaborator

remi-gelinas commented May 13, 2024

Odd.... Triage was the permission default set on the team for the repo. Since it says it can "manage pull requests", I assumed that was sufficient for merging. Weird - I've bumped it to Write for the teams. Can you confirm if you can merge the PR now @purcell ?

@purcell purcell merged commit 7ca2769 into nix-community:trunk May 14, 2024
16 checks passed
@purcell
Copy link
Member

purcell commented May 14, 2024

Yes, worked great, thanks! (Also merged #31)

@purcell
Copy link
Member

purcell commented May 14, 2024

The GitHub permission scheme is a bit confusing tbh, between team permissions, org permissions and individual repositories.

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.

4 participants