From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
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 <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
index 64553523e..000000000
--- 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
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