[m-rev.] diff: library grades from a file

[Zoltan Somogyi]

configure.log:
	Allow the set of library grades to be specified in a file named
	.enable_lib_grades, rather than on the command line. This is easier
	when invoking configure repeatedly.

Zoltan.

Index: configure.in
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/configure.in,v
retrieving revision 1.418
diff -u -b -r1.418 configure.in
--- configure.in	19 Jun 2005 02:14:16 -0000	1.418
+++ configure.in	29 Jun 2005 06:35:33 -0000
@@ -2796,6 +2796,11 @@
 
 # Allow the user to override the default list of library grades
 
+if test "$enable_libgrades_given" = no -a -f .enable_lib_grades ; then
+	enable_libgrades=`cat .enable_lib_grades`
+	enable_libgrades_given=yes
+fi
+
 if test "$enable_libgrades_given" = yes; then
 	if test "$enable_libgrades" = no; then
 		AC_MSG_ERROR(
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------