summaryrefslogtreecommitdiff
path: root/test-suite/coq-makefile/template/init.sh
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/coq-makefile/template/init.sh')
-rwxr-xr-xtest-suite/coq-makefile/template/init.sh3
1 files changed, 2 insertions, 1 deletions
diff --git a/test-suite/coq-makefile/template/init.sh b/test-suite/coq-makefile/template/init.sh
index e19d168c..2e066d30 100755
--- a/test-suite/coq-makefile/template/init.sh
+++ b/test-suite/coq-makefile/template/init.sh
@@ -1,10 +1,11 @@
+#!/bin/sh
. ../template/path-init.sh
rm -rf _test
mkdir _test
find . -maxdepth 1 -not -name . -not -name _test -exec cp -r '{}' -t _test ';'
-cd _test
+cd _test || exit 1
mkdir -p src
mkdir -p theories/sub