From 5bf25dfce23da1cee04b1c886e026f0dbc902c9c Mon Sep 17 00:00:00 2001
From: charguer
Date: Fri, 8 Nov 2019 11:06:10 +0100
Subject: From CoqIDE or -vos or -vok compilation, load .vo when .vos is
 missing (fixing bug #11057). With this new behavior, it is not needed to .vos
 files in user contribs. Also, this commit adds a feature: upon creation of a
 .vo file, an empty .vok file is touched.

---
 test-suite/coq-makefile/coqdoc1/run.sh   | 2 --
 test-suite/coq-makefile/coqdoc2/run.sh   | 2 --
 test-suite/coq-makefile/mlpack1/run.sh   | 1 -
 test-suite/coq-makefile/mlpack2/run.sh   | 1 -
 test-suite/coq-makefile/multiroot/run.sh | 2 --
 test-suite/coq-makefile/native1/run.sh   | 1 -
 test-suite/coq-makefile/plugin1/run.sh   | 1 -
 test-suite/coq-makefile/plugin2/run.sh   | 1 -
 test-suite/coq-makefile/plugin3/run.sh   | 1 -
 9 files changed, 12 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/coq-makefile/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh
index 0d9b9ea867..88237815b1 100755
--- a/test-suite/coq-makefile/coqdoc1/run.sh
+++ b/test-suite/coq-makefile/coqdoc1/run.sh
@@ -28,12 +28,10 @@ sort -u > desired <<EOT
 ./test/test.glob
 ./test/test.v
 ./test/test.vo
-./test/test.vos
 ./test/sub
 ./test/sub/testsub.glob
 ./test/sub/testsub.v
 ./test/sub/testsub.vo
-./test/sub/testsub.vos
 ./test/mlihtml
 ./test/mlihtml/index_exceptions.html
 ./test/mlihtml/index.html
diff --git a/test-suite/coq-makefile/coqdoc2/run.sh b/test-suite/coq-makefile/coqdoc2/run.sh
index 852ac372f4..5811dd17e4 100755
--- a/test-suite/coq-makefile/coqdoc2/run.sh
+++ b/test-suite/coq-makefile/coqdoc2/run.sh
@@ -26,12 +26,10 @@ sort -u > desired <<EOT
 ./test/test.glob
 ./test/test.v
 ./test/test.vo
-./test/test.vos
 ./test/sub
 ./test/sub/testsub.glob
 ./test/sub/testsub.v
 ./test/sub/testsub.vo
-./test/sub/testsub.vos
 ./test/mlihtml
 ./test/mlihtml/index_exceptions.html
 ./test/mlihtml/index.html
diff --git a/test-suite/coq-makefile/mlpack1/run.sh b/test-suite/coq-makefile/mlpack1/run.sh
index 1303aa90b6..bbd2fc460c 100755
--- a/test-suite/coq-makefile/mlpack1/run.sh
+++ b/test-suite/coq-makefile/mlpack1/run.sh
@@ -19,6 +19,5 @@ sort > desired <<EOT
 ./test/test_plugin.cmxs
 ./test/test.v
 ./test/test.vo
-./test/test.vos
 EOT
 exec diff -u desired actual
diff --git a/test-suite/coq-makefile/mlpack2/run.sh b/test-suite/coq-makefile/mlpack2/run.sh
index 1303aa90b6..bbd2fc460c 100755
--- a/test-suite/coq-makefile/mlpack2/run.sh
+++ b/test-suite/coq-makefile/mlpack2/run.sh
@@ -19,6 +19,5 @@ sort > desired <<EOT
 ./test/test_plugin.cmxs
 ./test/test.v
 ./test/test.vo
-./test/test.vos
 EOT
 exec diff -u desired actual
diff --git a/test-suite/coq-makefile/multiroot/run.sh b/test-suite/coq-makefile/multiroot/run.sh
index 3a5425c8bf..45bf1481df 100755
--- a/test-suite/coq-makefile/multiroot/run.sh
+++ b/test-suite/coq-makefile/multiroot/run.sh
@@ -29,12 +29,10 @@ sort > desired <<EOT
 ./test/test_plugin.cmxs
 ./test/test.v
 ./test/test.vo
-./test/test.vos
 ./test2
 ./test2/test.glob
 ./test2/test.v
 ./test2/test.vo
-./test2/test.vos
 ./orphan_test_test2_test
 ./orphan_test_test2_test/html
 ./orphan_test_test2_test/html/coqdoc.css
diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh
index 588de82613..8f9ab9a711 100755
--- a/test-suite/coq-makefile/native1/run.sh
+++ b/test-suite/coq-makefile/native1/run.sh
@@ -22,7 +22,6 @@ sort > desired <<EOT
 ./test/test_plugin.cmxs
 ./test/test.v
 ./test/test.vo
-./test/test.vos
 ./test/.coq-native
 ./test/.coq-native/Ntest_test.cmi
 ./test/.coq-native/Ntest_test.cmx
diff --git a/test-suite/coq-makefile/plugin1/run.sh b/test-suite/coq-makefile/plugin1/run.sh
index cd47187582..1e2bd979b3 100755
--- a/test-suite/coq-makefile/plugin1/run.sh
+++ b/test-suite/coq-makefile/plugin1/run.sh
@@ -22,6 +22,5 @@ sort > desired <<EOT
 ./test/test_plugin.cmxs
 ./test/test.v
 ./test/test.vo
-./test/test.vos
 EOT
 exec diff -u desired actual
diff --git a/test-suite/coq-makefile/plugin2/run.sh b/test-suite/coq-makefile/plugin2/run.sh
index cd47187582..1e2bd979b3 100755
--- a/test-suite/coq-makefile/plugin2/run.sh
+++ b/test-suite/coq-makefile/plugin2/run.sh
@@ -22,6 +22,5 @@ sort > desired <<EOT
 ./test/test_plugin.cmxs
 ./test/test.v
 ./test/test.vo
-./test/test.vos
 EOT
 exec diff -u desired actual
diff --git a/test-suite/coq-makefile/plugin3/run.sh b/test-suite/coq-makefile/plugin3/run.sh
index cd47187582..1e2bd979b3 100755
--- a/test-suite/coq-makefile/plugin3/run.sh
+++ b/test-suite/coq-makefile/plugin3/run.sh
@@ -22,6 +22,5 @@ sort > desired <<EOT
 ./test/test_plugin.cmxs
 ./test/test.v
 ./test/test.vo
-./test/test.vos
 EOT
 exec diff -u desired actual
-- 
cgit v1.2.3