diff options
Diffstat (limited to 'pg')
-rwxr-xr-x | pg | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -11,7 +11,7 @@ VARIANT=$ARCH/`sed -n -e 's/^VARIANT=//p' Makefile.config` make -q ${1}o || { make -n ${1}o | grep -v "\\b${1}\\b" | \ (while read cmd; do - $cmd || exit 2 + sh -c "$cmd" || exit 2 done) } COQPROGNAME="coqtop" |