src/Pure/Makefile
changeset 2023 aa25f20c5d8b
parent 1671 608196238072
child 2094 2061df98aab5
     1.1 --- a/src/Pure/Makefile	Tue Sep 24 13:54:27 1996 +0200
     1.2 +++ b/src/Pure/Makefile	Wed Sep 25 11:10:31 1996 +0200
     1.3 @@ -41,7 +41,8 @@
     1.4  	poly*)	echo database=$${ML_DBASE:?'No Poly/ML database specified'};\
     1.5  		cp $(ML_DBASE) $(BIN)/Pure; chmod u+w $(BIN)/Pure;\
     1.6  		echo 'PolyML.use"POLY";use"ROOT" handle _=> exit 1;' \
     1.7 -                  | $(COMP) $(BIN)/Pure;;\
     1.8 +                  | $(COMP) $(BIN)/Pure;\
     1.9 +		discgarb -c $(BIN)/Pure;;\
    1.10  	sml*)	if [ ! '(' -d $${ISABELLEBIN:?} -a -w $${ISABELLEBIN:?} ')' ];\
    1.11             	then echo Bad value for ISABELLEBIN: \
    1.12                  	$(BIN) is not a writable directory; \