Calls discgarb -c to realize dramatic space savings!
authorpaulson
Wed Sep 25 11:10:31 1996 +0200 (1996-09-25)
changeset 2023aa25f20c5d8b
parent 2022 9d47e2962edd
child 2024 909153d8318f
Calls discgarb -c to realize dramatic space savings!
src/CCL/Makefile
src/CTT/Makefile
src/Cube/Makefile
src/FOL/Makefile
src/FOLP/Makefile
src/HOL/Auth/Makefile
src/HOL/Makefile
src/HOLCF/Makefile
src/LCF/Makefile
src/LK/Makefile
src/Modal/Makefile
src/Pure/Makefile
src/ZF/Makefile
     1.1 --- a/src/CCL/Makefile	Tue Sep 24 13:54:27 1996 +0200
     1.2 +++ b/src/CCL/Makefile	Wed Sep 25 11:10:31 1996 +0200
     1.3 @@ -43,7 +43,8 @@
     1.4                  then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/CCL;\
     1.5                  else echo 'open PolyML; exit_use_dir".";' \
     1.6                         | $(COMP) $(BIN)/CCL;\
     1.7 -                fi;;\
     1.8 +                fi;\
     1.9 +		discgarb -c $(BIN)/CCL;;\
    1.10  	sml*)   if [ "$${MAKE_HTML}" = "true" ]; \
    1.11                  then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/CCL" banner;' | $(BIN)/FOL;\
    1.12                  elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
     2.1 --- a/src/CTT/Makefile	Tue Sep 24 13:54:27 1996 +0200
     2.2 +++ b/src/CTT/Makefile	Wed Sep 25 11:10:31 1996 +0200
     2.3 @@ -42,7 +42,8 @@
     2.4                  then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/CTT;\
     2.5                  else echo 'open PolyML; exit_use_dir".";' \
     2.6                         | $(COMP) $(BIN)/CTT;\
     2.7 -                fi;;\
     2.8 +                fi;\
     2.9 +		discgarb -c $(BIN)/CTT;;\
    2.10  	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
    2.11                  then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/CTT" banner;' | $(BIN)/Pure;\
    2.12                  elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
     3.1 --- a/src/Cube/Makefile	Tue Sep 24 13:54:27 1996 +0200
     3.2 +++ b/src/Cube/Makefile	Wed Sep 25 11:10:31 1996 +0200
     3.3 @@ -35,7 +35,8 @@
     3.4                  then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/Cube;\
     3.5                  else echo 'open PolyML; exit_use_dir".";' \
     3.6  		       | $(COMP) $(BIN)/Cube;\
     3.7 -                fi;;\
     3.8 +                fi;\
     3.9 +		discgarb -c $(BIN)/Cube;;\
    3.10  	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
    3.11                  then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/Cube" banner;' | $(BIN)/Pure;\
    3.12                  elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
     4.1 --- a/src/FOL/Makefile	Tue Sep 24 13:54:27 1996 +0200
     4.2 +++ b/src/FOL/Makefile	Wed Sep 25 11:10:31 1996 +0200
     4.3 @@ -45,7 +45,8 @@
     4.4                  then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/FOL;\
     4.5                  else echo 'open PolyML; exit_use_dir".";' \
     4.6                         | $(COMP) $(BIN)/FOL;\
     4.7 -                fi;;\
     4.8 +                fi;\
     4.9 +		discgarb -c $(BIN)/FOL;;\
    4.10  	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
    4.11                  then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/FOL" banner;' | $(BIN)/Pure;\
    4.12                  elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
     5.1 --- a/src/FOLP/Makefile	Tue Sep 24 13:54:27 1996 +0200
     5.2 +++ b/src/FOLP/Makefile	Wed Sep 25 11:10:31 1996 +0200
     5.3 @@ -39,7 +39,8 @@
     5.4                  then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/FOLP;\
     5.5                  else echo 'open PolyML; exit_use_dir".";' \
     5.6  		       | $(COMP) $(BIN)/FOLP;\
     5.7 -                fi;;\
     5.8 +                fi;\
     5.9 +		discgarb -c $(BIN)/FOLP;;\
    5.10  	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
    5.11                  then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/FOLP" banner;' | $(BIN)/Pure;\
    5.12                  elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
     6.1 --- a/src/HOL/Auth/Makefile	Tue Sep 24 13:54:27 1996 +0200
     6.2 +++ b/src/HOL/Auth/Makefile	Wed Sep 25 11:10:31 1996 +0200
     6.3 @@ -24,7 +24,8 @@
     6.4                  then echo 'open PolyML; init_html(); exit_use"DB-ROOT.ML";                               make_html := false;' | $(COMP) $(BIN)/Auth;\
     6.5                  else echo 'open PolyML; exit_use"DB-ROOT.ML";' \
     6.6                         | $(COMP) $(BIN)/Auth;\
     6.7 -                fi;;\
     6.8 +                fi;\
     6.9 +		discgarb -c $(BIN)/Auth;;\
    6.10  	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
    6.11                  then echo 'init_html(); exit_use"DB-ROOT.ML";                                            xML"$(BIN)/Auth" banner;' | $(BIN)/HOL;\
    6.12                  elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
     7.1 --- a/src/HOL/Makefile	Tue Sep 24 13:54:27 1996 +0200
     7.2 +++ b/src/HOL/Makefile	Wed Sep 25 11:10:31 1996 +0200
     7.3 @@ -48,7 +48,8 @@
     7.4                  then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/HOL;\
     7.5                  else echo 'open PolyML; exit_use_dir".";' \
     7.6                         | $(COMP) $(BIN)/HOL;\
     7.7 -                fi;;\
     7.8 +                fi;\
     7.9 +		discgarb -c $(BIN)/HOL;;\
    7.10  	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
    7.11                  then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/HOL" banner;' | $(BIN)/Pure;\
    7.12                  elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
     8.1 --- a/src/HOLCF/Makefile	Tue Sep 24 13:54:27 1996 +0200
     8.2 +++ b/src/HOLCF/Makefile	Wed Sep 25 11:10:31 1996 +0200
     8.3 @@ -43,7 +43,8 @@
     8.4                  then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/HOLCF;\
     8.5                  else echo 'open PolyML; exit_use_dir".";' \
     8.6  		       | $(COMP) $(BIN)/HOLCF;\
     8.7 -                fi;;\
     8.8 +                fi;\
     8.9 +		discgarb -c $(BIN)/HOLCF;;\
    8.10  	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
    8.11                  then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/HOLCF" banner;' | $(BIN)/HOL;\
    8.12                  elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
     9.1 --- a/src/LCF/Makefile	Tue Sep 24 13:54:27 1996 +0200
     9.2 +++ b/src/LCF/Makefile	Wed Sep 25 11:10:31 1996 +0200
     9.3 @@ -34,7 +34,8 @@
     9.4                  then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/LCF;\
     9.5                  else echo 'open PolyML; exit_use_dir".";' \
     9.6                         | $(COMP) $(BIN)/LCF;\
     9.7 -                fi;;\
     9.8 +                fi;\
     9.9 +		discgarb -c $(BIN)/LCF;;\
    9.10  	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
    9.11                  then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/LCF" banner;' | $(BIN)/FOL;\
    9.12                  elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    10.1 --- a/src/LK/Makefile	Tue Sep 24 13:54:27 1996 +0200
    10.2 +++ b/src/LK/Makefile	Wed Sep 25 11:10:31 1996 +0200
    10.3 @@ -34,7 +34,8 @@
    10.4  		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    10.5                  then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/LK;\
    10.6                  else echo 'open PolyML; exit_use_dir".";' | $(COMP) $(BIN)/LK;\
    10.7 -                fi;;\
    10.8 +                fi;\
    10.9 +		discgarb -c $(BIN)/LK;;\
   10.10  	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
   10.11                  then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/LK" banner;' | $(BIN)/Pure;\
   10.12                  elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    11.1 --- a/src/Modal/Makefile	Tue Sep 24 13:54:27 1996 +0200
    11.2 +++ b/src/Modal/Makefile	Wed Sep 25 11:10:31 1996 +0200
    11.3 @@ -35,7 +35,8 @@
    11.4                  then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/Modal;\
    11.5                  else echo 'open PolyML; exit_use_dir".";' \
    11.6  		       | $(COMP) $(BIN)/Modal;\
    11.7 -                fi;;\
    11.8 +                fi;\
    11.9 +		discgarb -c $(BIN)/Modal;;\
   11.10  	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
   11.11                  then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/Modal" banner;' | $(BIN)/LK;\
   11.12                  elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    12.1 --- a/src/Pure/Makefile	Tue Sep 24 13:54:27 1996 +0200
    12.2 +++ b/src/Pure/Makefile	Wed Sep 25 11:10:31 1996 +0200
    12.3 @@ -41,7 +41,8 @@
    12.4  	poly*)	echo database=$${ML_DBASE:?'No Poly/ML database specified'};\
    12.5  		cp $(ML_DBASE) $(BIN)/Pure; chmod u+w $(BIN)/Pure;\
    12.6  		echo 'PolyML.use"POLY";use"ROOT" handle _=> exit 1;' \
    12.7 -                  | $(COMP) $(BIN)/Pure;;\
    12.8 +                  | $(COMP) $(BIN)/Pure;\
    12.9 +		discgarb -c $(BIN)/Pure;;\
   12.10  	sml*)	if [ ! '(' -d $${ISABELLEBIN:?} -a -w $${ISABELLEBIN:?} ')' ];\
   12.11             	then echo Bad value for ISABELLEBIN: \
   12.12                  	$(BIN) is not a writable directory; \
    13.1 --- a/src/ZF/Makefile	Tue Sep 24 13:54:27 1996 +0200
    13.2 +++ b/src/ZF/Makefile	Wed Sep 25 11:10:31 1996 +0200
    13.3 @@ -44,7 +44,8 @@
    13.4                  then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/ZF;\
    13.5                  else echo 'open PolyML; exit_use_dir".";' \
    13.6                         | $(COMP) $(BIN)/ZF;\
    13.7 -                fi;;\
    13.8 +                fi;\
    13.9 +		discgarb -c $(BIN)/ZF;;\
   13.10  	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
   13.11                  then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/ZF" banner;' | $(BIN)/FOL;\
   13.12                  elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\