]> matita.cs.unibo.it Git - helm.git/blob - helm/configuration/install
83fe700105bd72c83c14855a069040152fe36fe4
[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 mkdir -p $ROOT/local/lib/helm
12 mkdir -p $ROOT/local/etc/helm
13
14 echo cp local/lib/helm/configuration.pl $ROOT/local/lib/helm/
15 cp local/lib/helm/configuration.pl $ROOT/local/lib/helm/
16
17 echo cp local/etc/helm/configuration.xml $ROOT/local/etc/helm/
18 cp local/etc/helm/configuration.xml $ROOT/local/etc/helm/
19
20 echo cp local/etc/helm/configuration.dtd $ROOT/local/etc/helm/
21 cp local/etc/helm/configuration.dtd $ROOT/local/etc/helm/