[m-rev.] diff: default bootcheck grade

[Zoltan Somogyi]

tools/bootcheck:
	Allow a workspace to have a file, .BOOT_GRADE, that sets the default
	grade for bootchecks.

	Do not require .KEEP_OBJS, which turns on --keep-objs by default,
	to be a directory.

Zoltan.

Index: bootcheck
===================================================================
RCS file: /home/mercury1/repository/mercury/tools/bootcheck,v
retrieving revision 1.128
diff -u -b -r1.128 bootcheck
--- bootcheck	2002/06/22 19:16:13	1.128
+++ bootcheck	2002/07/18 10:15:34
@@ -142,9 +142,14 @@
 write_out_profile_data=false
 type_stats=""
 
-if test -d .KEEP_OBJS
+if test -e .KEEP_OBJS
 then
 	keep_objs=true
+fi
+
+if test -f .BOOT_GRADE
+then
+	grade=`cat .BOOT_GRADE`
 fi
 
 # If you change these, you will also need to change scripts/ml.in,
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------