Proposed changes to meta.yml

[Casteran]

@palmskog

I wrote a new version (without 8.11 and with references to Russel's work) on the branch remove-8-11,
but the script generate.sh fails (I used the opam version of mustache)

---.opam: File name too long
Fatal error: exception Ezjsonm.Parse_error(870828711, "JSON.of_buffer illegal number (---)")
Generating resources/index.md...
Fatal error: exception Ezjsonm.Parse_error(870828711, "JSON.of_buffer illegal number (---)")
Fatal error: exception Ezjsonm.Parse_error(870828711, "JSON.of_buffer illegal number (---)")
Fatal error: exception Ezjsonm.Parse_error(870828711, "JSON.of_buffer illegal number (---)")
Generating .github/workflows/nix-action.yml...
Fatal error: exception Ezjsonm.Parse_error(870828711, "JSON.of_buffer illegal number (---)")
Fatal error: exception Ezjsonm.Parse_error(870828711, "JSON.of_buffer illegal number (---)")
Generating .travis.yml...
Fatal error: exception Ezjsonm.Parse_error(870828711, "JSON.of_buffer illegal number (---)")

[palmskog]

@Casteran unfortunately the opam version of mustache does not support the format we use (YAML). You can see that there is some work in the pipeline that might fix this, but it is not there yet: rgrinberg/ocaml-mustache#45

[Zimmi48]

You can use ruby-mustache instead, which is available as a Debian / Ubuntu package.

[Casteran]

@Zimmi48 @palmskog
I've just installed ruby-mustache on my Mac.
I ran (successfully) the script on the remove-8-11 branch, but I got the following message while trying to push.

! [remote rejected] remove-8-11 -> remove-8-11 (refusing to allow a Personal Access Token to create or update workflow .github/workflows/docker-action.yml without workflow scope)

Is this a problem of access rights ?

[Zimmi48]

Are you using a GitHub-specific tool like GitHub desktop? I don't think you can get this problem if you push using the git command-line directly authenticating with ssh or username/password.

[Casteran]

In fact, when generating a personal access token for GitHub, I forgot to add the workflow permission. I succeeded in pushing the branch remove-8-11, and made a PR.

…

Le 18 janv. 2021 à 14:26, Théo Zimmermann ***@***.***> a écrit : Are you using a GitHub-specific tool like GitHub desktop? I don't think you can get this problem if you push using the git command-line directly authenticating with ssh or username/password. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#24 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AJW6FCU3YBSAZX3ZYULCU4DS2QZG7ANCNFSM4WCG3PSQ>.