mercurylang/mercury
1
0
Fork 0
mirror of https://github.com/Mercury-Language/mercury.git synced 2025-12-11 11:53:51 +00:00
Code Issues Projects Releases Wiki Activity

Make re-configuring things a little more robust.

Browse Source 
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.
This commit is contained in:
Julien Fischer
2008-11-04 02:34:13 +00:00
parent c21694efbb
commit 56ef0245c3
1 changed files with 3 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

3
scripts/mercury_config.in
View File

@@ -42,6 +42,7 @@ Configure options:
"
#---------------------------------------------------------------------------#
default_grade=${MERCURY_DEFAULT_GRADE-@DEFAULT_GRADE@}
input_prefix=@prefix@
output_prefix=@CONFIG_PREFIX@
exe_ext=@EXT_FOR_EXE@
@@ -159,12 +160,14 @@ cd $TMPDIR
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