# HG changeset patch
# User wenzelm
# Date 875538687 -7200
# Node ID 6fccb16a7e3a8da594007a57a7e10b42f5e6bb7d
# Parent  daa5ac720678f72ababbbcd040b85a1ae3699d84
obsolete;

diff -r daa5ac720678 -r 6fccb16a7e3a src/Tools/make-all-nj
--- a/src/Tools/make-all-nj	Mon Sep 29 15:08:47 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-#! /bin/sh
-#Make entire system using Standard ML of New Jersey
-#Pathnames will have to be modified for your site
-ISABELLEBIN=/homes/`whoami`/bin
-ISABELLECOMP=sml
-export ISABELLEBIN ISABELLECOMP 
-nohup make-all $*
diff -r daa5ac720678 -r 6fccb16a7e3a src/Tools/make-all-poly
--- a/src/Tools/make-all-poly	Mon Sep 29 15:08:47 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-#! /bin/sh
-#$Id$
-#Make entire system using Poly/ML
-#Pathnames will have to be modified for your site
-ML_DBASE=/usr/groups/theory/poly/polyml/`arch`/ML_dbase
-ISABELLEBIN=/homes/`whoami`/dbases
-ISABELLECOMP="poly -noDisplay -h 15000"
-export ML_DBASE ISABELLEBIN ISABELLECOMP 
-nohup make-all $*
diff -r daa5ac720678 -r 6fccb16a7e3a src/Tools/rm_html.sh
--- a/src/Tools/rm_html.sh	Mon Sep 29 15:08:47 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-#!/bin/csh
-# Executed from the main Isabelle directory, this script removes all files
-# made when Isabelle was used with set MAKE_HTML
-
-rm */.theory_list.txt */*/.theory_list.txt */*/*/.theory_list.txt \
-   */index.html */*/index.html */*/*/index.html \
-   */.*.html */*/.*.html */*/*/.*.html