Removed stuff no longer in use.

diff --git a/helm/scripts/.cvsignore b/helm/scripts/.cvsignore
deleted file mode 100644 (file)
index 852e674..0000000
--- 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 (file)
index be6ba21..0000000
--- a/helm/scripts/Makefile
+++ /dev/null
@@ -1,16 +0,0 @@
-
-all: 
-       - chmod ug+w phd*rc
-       ./makeit phd <template.cshrc >phd_mowgli.cshrc
-       ./makeit phd <template.rc >phd_mowgli.rc
-       ./makeit marcello <template.cshrc >phd_marcello_mowgli.cshrc
-       ./makeit marcello <template.rc >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 (executable)
index 6455352..0000000
--- a/helm/scripts/makeit
+++ /dev/null
@@ -1,10 +0,0 @@
-#!/bin/sh
-
-if test $# != 1; then
-       echo "Usage: makeit <from>"
-       echo
-  echo "<from> 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 (file)
index 320dbcd..0000000
--- 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 (file)
index ea10462..0000000
--- 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