X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FEXPORT%2Fexportcoq%2FMakefile;h=5026ec526f835352a9053fa27bd82cb8a7d61f32;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=79c7463a046086eb5209a051ea5a58d61b2eeda7;hpb=5cc1f56f25e23f8132b578f9ad46ac9e27979cb4;p=helm.git

diff --git a/helm/EXPORT/exportcoq/Makefile b/helm/EXPORT/exportcoq/Makefile
index 79c7463a0..5026ec526 100644
--- a/helm/EXPORT/exportcoq/Makefile
+++ b/helm/EXPORT/exportcoq/Makefile
@@ -1,7 +1,7 @@
 all: objects theories
 
 objects:
-	echo "Load Verbose provacoq." | ~/V7/bin/coqtop.byte
+	echo "Load Verbose provacoq." | coqtop.byte
 
 theories:
 	./exporttheories.sh