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/plugin2/run.sh | 1 - 1 file changed, 1 deletion(-) (limited to 'test-suite/coq-makefile/plugin2') 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 <