[m-rev.] diff: .configured_library_grades

[Zoltan Somogyi]

configure.in:
	Record the set of library grades to install in a file named
	.configured_library_grades. This is useful when you want to know
	how many grades are still left to do during a "make install".

Zoltan.

cvs diff: Diffing .
Index: configure.in
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/configure.in,v
retrieving revision 1.615
diff -u -b -r1.615 configure.in
--- configure.in	23 May 2012 17:03:19 -0000	1.615
+++ configure.in	14 Jun 2012 02:05:13 -0000
@@ -5521,9 +5521,11 @@
 MERCURY_MSG("")
 num_installed_grades=0
 MERCURY_MSG("the set of library grades to install will be")
+> .configured_library_grades
 for grade in $LIBGRADES
 do
     MERCURY_MSG("   $grade")
+    echo "$grade" >> .configured_library_grades
     num_installed_grades=`expr $num_installed_grades + 1`
 done
 MERCURY_MSG("")
--------------------------------------------------------------------------
mercury-reviews mailing list
Post messages to:       mercury-reviews at csse.unimelb.edu.au
Administrative Queries: owner-mercury-reviews at csse.unimelb.edu.au
Subscriptions:          mercury-reviews-request at csse.unimelb.edu.au
--------------------------------------------------------------------------