]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/configuration/install
install script added
[helm.git] / helm / configuration / install
diff --git a/helm/configuration/install b/helm/configuration/install
new file mode 100755 (executable)
index 0000000..5b19af1
--- /dev/null
@@ -0,0 +1,18 @@
+#!/bin/sh
+
+echo "********************************************************"
+echo "* Insert the root dir \$root                           *"
+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"
+
+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/configuration.dtd $ROOT/local/etc/helm/
+cp local/etc/helm/configuration.dtd $ROOT/local/etc/helm/