]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/configuration/install
All files previously in local/$i/helm moved in $i
[helm.git] / helm / configuration / install
index de250745931aaac0dba98b705bebf76cdfd1ee6f..f84b12cb31f58f6733e5067aec9ba1d8ddd4a166 100755 (executable)
@@ -8,11 +8,12 @@ echo "********************************************************"
 echo -n "\$root="
 read ROOT
 
+mkdir -p $ROOT/local/lib/helm
+mkdir -p $ROOT/local/etc/helm
+
 echo cp local/lib/helm/configuration.pl $ROOT/local/lib/helm/
 cp local/lib/helm/configuration.pl $ROOT/local/lib/helm/
 
-echo cp local/etc/helm/configuration.xml $ROOT/local/etc/helm/
-cp local/etc/helm/configuration.xml $ROOT/local/etc/helm/
+echo cp local/etc/helm/* $ROOT/local/etc/helm/
+cp local/etc/helm/* $ROOT/local/etc/helm/
 
-echo cp local/etc/helm/configuration.dtd $ROOT/local/etc/helm/
-cp local/etc/helm/configuration.dtd $ROOT/local/etc/helm/