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
# - Adds to the make file for the current project the command to set the opam switch, eval is fine in bash, no further questions needed.
echo 'eval \"$(opam env --set-switch --switch=$SWITCH)\"' >> coq-projects/$project/make.sh
the one with single quotes evaluated $(...) and thus make the main.sh depedent on the machine and breaks in clusters with multiple servers.
To write the literal string echo "eval "$(opam env --set-switch --switch=$SWITCH)"" without executing the $(opam env --set-switch --switch=$SWITCH) command substitution, you can use single quotes instead of double quotes.
In Bash, single quotes preserve the literal value of all characters within the quotes, so variable substitution and command substitution won't occur. Here's the modified code:
echo 'echo "eval \"$(opam env --set-switch --switch=$SWITCH)\""' >> coq-projects/$project/make.sh
By using single quotes instead of double quotes, the $(opam env --set-switch --switch=$SWITCH)
command substitution will be treated as a literal string and not evaluated.
The text was updated successfully, but these errors were encountered:
You should do this:
the one with single quotes evaluated $(...) and thus make the main.sh depedent on the machine and breaks in clusters with multiple servers.
To write the literal string echo "eval "$(opam env --set-switch --switch=$SWITCH)"" without executing the $(opam env --set-switch --switch=$SWITCH) command substitution, you can use single quotes instead of double quotes.
In Bash, single quotes preserve the literal value of all characters within the quotes, so variable substitution and command substitution won't occur. Here's the modified code:
command substitution will be treated as a literal string and not evaluated.
The text was updated successfully, but these errors were encountered: