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.sh17
1 files changed, 17 insertions, 0 deletions
diff --git a/test-suite/coq-makefile/template/init.sh b/test-suite/coq-makefile/template/init.sh
new file mode 100755
index 00000000..e19d168c
--- /dev/null
+++ b/test-suite/coq-makefile/template/init.sh
@@ -0,0 +1,17 @@
+. ../template/path-init.sh
+
+rm -rf _test
+mkdir _test
+find . -maxdepth 1 -not -name . -not -name _test -exec cp -r '{}' -t _test ';'
+
+cd _test
+mkdir -p src
+mkdir -p theories/sub
+
+cp ../../template/theories/sub/testsub.v theories/sub
+cp ../../template/theories/test.v theories
+cp ../../template/src/test.ml4 src
+cp ../../template/src/test_aux.mli src
+cp ../../template/src/test.mli src
+cp ../../template/src/test_plugin.mlpack src
+cp ../../template/src/test_aux.ml src