Hi @Guillaume Melquiond, there is this test in misc which you wrote but I don't quite understand.
#!/usr/bin/env bash
set -e
export PATH=$BIN:$PATH
export OCAMLRUNPARAM=s=1
${coqc#"$BIN"} misc/aux11170.v
Isn't the bash ${string#substring}
syntax supposed to remove a substring? Could you explain what the intention with this test was?
IIRC ${var#prefix}
is standard (POSIX?) shell for remove prefix
from var (if present, otherwise keep var unchanged)
I already have coqc in the env, so would setting OCAMLRUNPARAM=s=1
and passing coqc
instead be enough?
I am not the original author of this code. I think it was @Gaëtan Gilbert . I guess that the motivation for this construct was to ensure that argv[0]
was the canonical name of coqc
.
https://github.com/coq/coq/pull/13431/files
Fair enough, I will get rid of the extra fluff then.
Sure, but I only copied an already existing testcase.
Ali Caglayan has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC