]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/configuration/install
Many bug fixed
[helm.git] / helm / configuration / install
index 5b19af19da846605db98fe2830b5b0c0ee79914a..de250745931aaac0dba98b705bebf76cdfd1ee6f 100755 (executable)
@@ -6,7 +6,7 @@ echo "* Files will be installed in \$root/local/lib/helm and *"
 echo "* in \$root/local/lib/etc/helm/                        *"
 echo "********************************************************"
 echo -n "\$root="
-read ROOT "buondi"
+read ROOT
 
 echo cp local/lib/helm/configuration.pl $ROOT/local/lib/helm/
 cp local/lib/helm/configuration.pl $ROOT/local/lib/helm/