From: Claudio Sacerdoti Coen Date: Wed, 18 Feb 2004 16:11:27 +0000 (+0000) Subject: Removed stuff no longer in use. X-Git-Tag: v0_0_4~143 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f90b82510f49539719a2e561519cca72a493334b;p=helm.git Removed stuff no longer in use. --- diff --git a/helm/scripts/.cvsignore b/helm/scripts/.cvsignore deleted file mode 100644 index 852e6747c..000000000 --- a/helm/scripts/.cvsignore +++ /dev/null @@ -1,16 +0,0 @@ -marcello.cshrc -marcello.rc -marcello_mowgli.cshrc -marcello_mowgli.rc -marcello_phd.cshrc -marcello_phd.rc -marcello_phd_mowgli.cshrc -marcello_phd_mowgli.rc -phd.cshrc -phd.rc -phd_marcello.cshrc -phd_marcello.rc -phd_marcello_mowgli.cshrc -phd_marcello_mowgli.rc -phd_mowgli.cshrc -phd_mowgli.rc diff --git a/helm/scripts/Makefile b/helm/scripts/Makefile deleted file mode 100644 index be6ba2198..000000000 --- a/helm/scripts/Makefile +++ /dev/null @@ -1,16 +0,0 @@ - -all: - - chmod ug+w phd*rc - ./makeit phd phd_mowgli.cshrc - ./makeit phd phd_mowgli.rc - ./makeit marcello phd_marcello_mowgli.cshrc - ./makeit marcello phd_marcello_mowgli.rc - chmod a+x phd*rc - chmod ug-w phd*rc - -clean: - rm -f phd*rc - -cleanbak: - rm -f *~ - diff --git a/helm/scripts/makeit b/helm/scripts/makeit deleted file mode 100755 index 64553523e..000000000 --- a/helm/scripts/makeit +++ /dev/null @@ -1,10 +0,0 @@ -#!/bin/sh - -if test $# != 1; then - echo "Usage: makeit " - echo - echo " is the machine we connect from" - exit 1 -fi - -sed -e "s/@FROM@/$1/" diff --git a/helm/scripts/template.cshrc b/helm/scripts/template.cshrc deleted file mode 100644 index 320dbcd5c..000000000 --- a/helm/scripts/template.cshrc +++ /dev/null @@ -1,29 +0,0 @@ - -set COQV=V7_mowgli -set WHERE=phd -set FROM=@FROM@ - -setenv CVS_RSH=ssh - -echo "Configuring HELM for $WHERE (from $FROM), Coq $COQV" - -setenv HELMROOT /projects/helm - -if ($WHERE == $FROM) then - set FONTROOT=$HELMROOT -else - if ($FROM == phd) then - set FONTROOT=/projects/helm - else - set FONTROOT=/home/projects/helm - endif -endif - -setenv MATHENGINECONF $HELMROOT/$COQV/$WHERE/local/etc/helm/helm-math-engine-configuration.xml - -umask 002 - -# Stix font -xset fp -xset fp+ $FONTROOT/fonts/mathematica/Type1/ -xset fp rehash diff --git a/helm/scripts/template.rc b/helm/scripts/template.rc deleted file mode 100644 index ea104625a..000000000 --- a/helm/scripts/template.rc +++ /dev/null @@ -1,29 +0,0 @@ - -COQV=V7_mowgli -WHERE=phd -FROM=@FROM@ - -export CVS_RSH=ssh - -echo "Configuring HELM for $WHERE (from $FROM), Coq $COQV" - -export HELMROOT=/projects/helm - -if test $WHERE = $FROM; then - FONTROOT=$HELMROOT -else - if test $FROM = phd; then - FONTROOT=/projects/helm - else - FONTROOT=/home/projects/helm - fi -fi - -export MATHENGINECONF=$HELMROOT/$COQV/$WHERE/local/etc/helm/helm-math-engine-configuration.xml - -umask 002 - -# Stix font -xset fp -xset fp+ $FONTROOT/fonts/mathematica/Type1/ -xset fp rehash