1 files changed, 1 insertions, 1 deletions
diff --git a/coq b/coq
index 97d4ca6..53ed140 100755
--- a/coq
+++ b/coq
@@ -9,7 +9,7 @@ VARIANT=`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)
 }