]> matita.cs.unibo.it Git - helm.git/commitdiff
install script added
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 31 Oct 2000 15:47:43 +0000 (15:47 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 31 Oct 2000 15:47:43 +0000 (15:47 +0000)
helm/configuration/install [new file with mode: 0755]

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/