...

diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile
index 9cba34bc70c771b0f3186d85937bc37e0ab339ee..bb4a33f7988400e07be463a4b5c7a4371b2c9d45 100644 (file)
--- a/helm/gTopLevel/Makefile
+++ b/helm/gTopLevel/Makefile
@@ -134,9 +134,9 @@ envtest: regtest
 envtest.opt: regtest.opt
        ./regtest.opt -dump $(INTESTS) 2> /dev/null
 librarytest: testlibrary
-       ./testlibrary -vars -varsprefix cic:/Coq index.txt 2>/dev/null >LOG &
+       ./testlibrary -vars -varsprefix cic:/Coq index.txt 2>/dev/null >LOG
 librarytest.opt: testlibrary.opt
-       ./testlibrary.opt -vars -varsprefix cic:/Coq index.txt 2>/dev/null >LOG &
+       ./testlibrary.opt -vars -varsprefix cic:/Coq index.txt 2>/dev/null >LOG
 
 MAIN = ./gTopLevel
 ARGS =