[m-rev.] trivial diff: remember library grades in mercury_config

[Julien Fischer]

scripts/mercury_config.in:
 	Remember what grades the libraries were installed in.  Pass this
 	information to configure when re-configuring.

Julien.

Index: scripts/mercury_config.in
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/scripts/mercury_config.in,v
retrieving revision 1.10
diff -u -r1.10 mercury_config.in
--- scripts/mercury_config.in	4 Nov 2008 02:34:13 -0000	1.10
+++ scripts/mercury_config.in	4 Nov 2008 04:04:34 -0000
@@ -43,6 +43,7 @@
  #---------------------------------------------------------------------------#

  default_grade=${MERCURY_DEFAULT_GRADE- at DEFAULT_GRADE@}
+libgrades="@LIBGRADES@"
  input_prefix=@prefix@
  output_prefix=@CONFIG_PREFIX@
  exe_ext=@EXT_FOR_EXE@
@@ -156,11 +157,14 @@
  mkdir $TMPDIR/deep_profiler || exit 1
  touch $TMPDIR/deep_profiler/DEEP_FLAGS.in || exit 1

+enable_libgrades=`echo $libgrades | sed 's/ /,/g'`
+
  cd $TMPDIR
  case $# in
  	0)
  		./configure @RECONFIGURE_ARGS@ \
  			--with-default-grade="$default_grade" \
+			--enable-libgrades="$enable_libgrades" \
  			--cache-file=/dev/null \
  			--prefix="$input_prefix" \
  			--enable-reconfigure="$output_prefix" || exit 1
@@ -168,6 +172,7 @@
  	*)
  		./configure @RECONFIGURE_ARGS@ "$@" \
  			--with-default-grade="$default_grade" \
+			--enable-libgrades="$enable_libgrades" \
  			--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
--------------------------------------------------------------------------