aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/coq-makefile
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/coq-makefile')
-rwxr-xr-xtest-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh2
-rwxr-xr-xtest-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh2
2 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh b/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh
index 378573957..e48f704a2 100755
--- a/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh
+++ b/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh
@@ -10,7 +10,7 @@ cat > _CoqProject <<EOT
./src/test.mli
EOT
-mkdir src
+mkdir -p src
cat > src/test_plugin.mllib <<EOT
Test
diff --git a/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh b/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh
index 1b57a356b..4a8f58655 100755
--- a/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh
+++ b/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh
@@ -11,7 +11,7 @@ cat > _CoqProject <<EOT
./src/test.mli
EOT
-mkdir src
+mkdir -p src
cat > src/test_plugin.mllib <<EOT
Test