[m-rev.] trivial diff: remember original default grade in mercury_config

[Julien Fischer]

Make re-configuring things a little more robust.

scripts/mercury_config.in:
 	Remember the original default grade that an installation was configured with
 	and use this as the "default" default grade when re-configuring.  The reason
 	for doing this is that the default grade as chosen be configure when
 	re-configuring may not be among those installed.  Users can still chose to
 	override the "default" default by setting MERCURY_DEFAULT_GRADE.

Julien.

Index: scripts/mercury_config.in
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/scripts/mercury_config.in,v
retrieving revision 1.9
diff -u -r1.9 mercury_config.in
--- scripts/mercury_config.in	3 Nov 2008 12:55:47 -0000	1.9
+++ scripts/mercury_config.in	4 Nov 2008 00:58:35 -0000
@@ -42,6 +42,7 @@
  "
  #---------------------------------------------------------------------------#

+default_grade=${MERCURY_DEFAULT_GRADE- at DEFAULT_GRADE@}
  input_prefix=@prefix@
  output_prefix=@CONFIG_PREFIX@
  exe_ext=@EXT_FOR_EXE@
@@ -159,12 +160,14 @@
  case $# in
  	0)
  		./configure @RECONFIGURE_ARGS@ \
+			--with-default-grade="$default_grade" \
  			--cache-file=/dev/null \
  			--prefix="$input_prefix" \
  			--enable-reconfigure="$output_prefix" || exit 1
  		;;
  	*)
  		./configure @RECONFIGURE_ARGS@ "$@" \
+			--with-default-grade="$default_grade" \
  			--cache-file=/dev/null \
  			--prefix="$input_prefix" \
  			--enable-reconfigure="$output_prefix" || exit 1

--------------------------------------------------------------------------
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
--------------------------------------------------------------------------