[m-rev.] diff: makebatch grade recording

[Zoltan Somogyi]

tools/makebatch:
	Record the grade of each compiler version in the corresponding
	parameter file, together with the options used in creating it.

Zoltan.

Index: makebatch
===================================================================
RCS file: /home/mercury1/repository/mercury/tools/makebatch,v
retrieving revision 1.13
diff -u -b -r1.13 makebatch
--- makebatch	2000/07/19 03:45:11	1.13
+++ makebatch	2001/04/26 09:23:01
@@ -154,6 +154,11 @@
 	fi
 
 	cp Mmake.stage.params batch/$batch.params.$visn
+	if $needgrade
+	then
+		echo "GRADE = $grade" >> batch/$batch.params.$visn
+	fi
+
 	echo starting bootcheck of version $visn
 	if tools/bootcheck $gradeopt -r $jfactor $runtests $objects > batch/$batch.out.$visn 2>&1
 	then
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------