]> matita.cs.unibo.it Git - helm.git/blob - helm/configuration/install
de250745931aaac0dba98b705bebf76cdfd1ee6f
[helm.git] / helm / configuration / install
1 #!/bin/sh
2
3 echo "********************************************************"
4 echo "* Insert the root dir \$root                           *"
5 echo "* Files will be installed in \$root/local/lib/helm and *"
6 echo "* in \$root/local/lib/etc/helm/                        *"
7 echo "********************************************************"
8 echo -n "\$root="
9 read ROOT
10
11 echo cp local/lib/helm/configuration.pl $ROOT/local/lib/helm/
12 cp local/lib/helm/configuration.pl $ROOT/local/lib/helm/
13
14 echo cp local/etc/helm/configuration.xml $ROOT/local/etc/helm/
15 cp local/etc/helm/configuration.xml $ROOT/local/etc/helm/
16
17 echo cp local/etc/helm/configuration.dtd $ROOT/local/etc/helm/
18 cp local/etc/helm/configuration.dtd $ROOT/local/etc/helm/