[m-rev.] diff: --enable-dmm-grades

Zoltan Somogyi zs at cs.mu.OZ.AU
Mon Aug 1 12:07:19 AEST 2005


configure.log:
	Add an option, --enable-dmm-grades, that asks for the installation of
	the grades that are useful only for debugging minimal model tabling.

	When getting the set of library grades from the .enable_lib_grades
	file, print a message to this effect.

Zoltan.

Index: configure.in
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/configure.in,v
retrieving revision 1.420
diff -u -b -r1.420 configure.in
--- configure.in	30 Jun 2005 06:08:32 -0000	1.420
+++ configure.in	29 Jul 2005 12:22:22 -0000
@@ -2649,6 +2649,10 @@
 [  --enable-mm-grades      install minimal model versions of the library],
 enable_mm_grades="$enableval",enable_mm_grades=no)
 
+AC_ARG_ENABLE(dmm-grades,
+[  --enable-dmm-grades      install minimal model debug versions of the library],
+enable_dmm_grades="$enableval",enable_dmm_grades=no)
+
 AC_ARG_ENABLE(hlc-prof-grades,
 [  --enable-hlc-prof-grades
                           install profiling versions of the high level C grade],
@@ -2678,6 +2682,7 @@
 	enable_prof_grades=no
 	enable_trail_grades=no
 	enable_mm_grades=no
+	enable_dmm_grades=no
 	enable_hlc_prof_grades=no
 	enable_par_grades=no
 	enable_dotnet_grades=no
@@ -2821,6 +2826,10 @@
 if test "$enable_mm_grades" = yes; then
 	LIBGRADES="$LIBGRADES $BEST_LLDS_BASE_GRADE.gc.mmsc \
 		$BEST_LLDS_BASE_GRADE.gc.mmsc.debug"
+	if test "$enable_dmm_grades" = yes; then
+		LIBGRADES="$LIBGRADES $BEST_LLDS_BASE_GRADE.gc.dmmsc \
+			$BEST_LLDS_BASE_GRADE.gc.dmmsc.debug"
+	fi
 fi
 
 # add `.debug' (--debug) and `.decldebug' (--decl-debug) grades
@@ -2851,6 +2860,7 @@
 # Allow the user to override the default list of library grades
 
 if test "$enable_libgrades_given" = no -a -f .enable_lib_grades ; then
+	MERCURY_MSG("using .enable_libgrades as the source for the set of grades to install")
 	enable_libgrades=`cat .enable_lib_grades`
 	enable_libgrades_given=yes
 fi
@@ -2897,6 +2907,8 @@
 	fi
 fi
 
+# The echo deletes the initial space character.
+LIBGRADES=`echo $LIBGRADES`
 MERCURY_MSG("using \`$LIBGRADES' as the set of library grades to install")
 
 LIBGRADE_OPTS=
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------



More information about the reviews mailing list