aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/coq-makefile/camldep/_CoqProject4
-rwxr-xr-xtest-suite/coq-makefile/camldep/run.sh17
2 files changed, 21 insertions, 0 deletions
diff --git a/test-suite/coq-makefile/camldep/_CoqProject b/test-suite/coq-makefile/camldep/_CoqProject
new file mode 100644
index 0000000000..0b7ebd14e4
--- /dev/null
+++ b/test-suite/coq-makefile/camldep/_CoqProject
@@ -0,0 +1,4 @@
+-Q . Foo
+-I src
+src/file1.mlg
+src/file2.ml
diff --git a/test-suite/coq-makefile/camldep/run.sh b/test-suite/coq-makefile/camldep/run.sh
new file mode 100755
index 0000000000..aa62ee56eb
--- /dev/null
+++ b/test-suite/coq-makefile/camldep/run.sh
@@ -0,0 +1,17 @@
+#!/usr/bin/env bash
+
+set -e
+export PATH=$COQBIN:$PATH
+export LC_ALL=C
+
+rm -rf _test
+mkdir _test
+cp _CoqProject _test/
+cd _test
+mkdir src
+
+echo '{ let foo = () }' > src/file1.mlg
+echo 'let bar = File1.foo' > src/file2.ml
+coq_makefile -f _CoqProject -o Makefile
+make src/file2.cmx
+[ -f src/file2.cmx ]