You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Hi @JasonGross, the error you raise is really a regular YAML error, I wasn't expecting that the current documentation was so misleading.
Actually, the export field should be a YAML string, containing a list (in informal sense) of space-separated shell variables.
No need for ' around each shell variable, because anyway, a variable name cannot contain a space.
So here, one can use export: "SKIP_VALIDATE COQCHKEXTRAFLAGS EXTRA_GH_REPORTIFY"
→ Do you think that the following line would be clearer in the doc?
export: 'OPAMWITHTEST OPAMWITHDOC' # space-separated list of variables
"space-separated list of variables" with an example of
'OPAMWITHTEST'
suggests to me that'foo' 'bar'
would be valid, but it's a very unhelpful syntax error:https://github.com/mit-plv/fiat-crypto/actions/runs/3206456319/workflow
The text was updated successfully, but these errors were encountered: