Ver código fonte

2004-06-22 Todd Berman <[email protected]>

        * configure: Patch from Mariano Su��rez-Alvarez
        <[email protected]> to make configure accept jhbuild style
        /prefix /usr options, and to continue past unknown options. Currently
        this patch is a bit spammy with multiple unknown options, anyone
        who is interested is welcome to fix this.

svn path=/trunk/mcs/; revision=30093
Todd Berman 21 anos atrás
pai
commit
eb6cb51857
2 arquivos alterados com 49 adições e 23 exclusões
  1. 8 0
      mcs/ChangeLog
  2. 41 23
      mcs/configure

+ 8 - 0
mcs/ChangeLog

@@ -1,3 +1,11 @@
+2004-06-22  Todd Berman  <[email protected]>
+
+	* configure: Patch from Mariano Suárez-Alvarez 
+	<[email protected]> to make configure accept jhbuild style
+	/prefix /usr options, and to continue past unknown options. Currently
+	this patch is a bit spammy with multiple unknown options, anyone
+	who is interested is welcome to fix this.
+
 2004-06-14  Raja R Harinath  <[email protected]>
 
 	* Makefile (all-profiles, clean-profiles): Simplify slightly.

+ 41 - 23
mcs/configure

@@ -12,29 +12,47 @@ help()
 prefix=/usr/local
 profile=default
 
-for a in $*; do
-	case $a in
-		--help)
-			help
-			exit 0
-			;;
-		--prefix=*)
-			prefix=`echo $a | sed 's/--prefix=//'`;
-			;;
-		--profile=*)
-			profile=`echo $a | sed 's/--profile=//'`;
-			if test ! -f build/profiles/$profile.make; then
-				echo ""
-				echo Error, profile $profile does not exist
-				help
-				exit 1;
-			fi
-			;;
-		*)
-			echo Unknown option: $a
-			help
-			exit 1
-	esac
+while [ $# -ne 0 ]; do
+  case $1 in
+    --help)  
+    	help
+    	exit 0
+	;;
+    --prefix=*)
+    	prefix=`echo $1 | sed 's/--prefix=//'`;
+	shift
+	;;
+    --prefix)
+        shift
+	prefix="$1"
+	shift
+	;;
+    --profile=*)
+	profile=`echo $1 | sed 's/--profile=//'`
+	shift
+	if test ! -f build/profiles/$profile.make; then
+	    echo ""
+	    echo Error, profile $profile does not exist
+	    help
+	    exit 1;
+	fi
+	;;
+    --profile)
+	shift
+	profile="$1"
+	shift
+	if test ! -f build/profiles/$profile.make; then
+	    echo ""
+	    echo Error, profile $profile does not exist
+	    help
+	    exit 1;
+	fi
+	;;
+    *)
+	echo Unknown option: $1
+	help
+	shift
+  esac
 done
 
 echo "prefix=$prefix" > build/config.make