[m-rev.] for review: bootcheck and make -k

[Zoltan Somogyi]

tools/bootcheck:
	Delete the option -M, which had no effect (it set the variable
	make_opts that was never consulted). Instead of putting -k (the
	keep-going flag) in the ignored make_opts variable, put it in the
	mmake_opts variable (which is used). This used to be the default;
	I don't know when it was screwed up.

Zoltan.

cvs diff: Diffing .
Index: bootcheck
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/tools/bootcheck,v
retrieving revision 1.180
diff -u -b -r1.180 bootcheck
--- bootcheck	25 Jan 2006 07:03:43 -0000	1.180
+++ bootcheck	23 Feb 2006 04:20:09 -0000
@@ -163,8 +163,7 @@
 extras=false
 jfactor=""
 keep_objs=false
-mmake_opts=""
-make_opts="-k"
+mmake_opts="-k"
 outfile=""
 runtests=true
 do_bootcheck=true
@@ -273,8 +272,6 @@
 
     -m|--mmake|--mmake-opts)
         mmake_opts="$mmake_opts $2"; shift ;;
-    -M|--make-opts)
-        make_opts="$make_opts $2"; shift ;;
 
     -o|--output-file)
         outfile="$2"; shift ;;
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------