[m-dev.] trivial diff: fix cut-and-paste bug in init_grade_options.sh-subr

[Fergus Henderson]

Estimated hours taken: 0.25

scripts/init_grade_options.sh-subr:
	Fix a cut-and-paste error: change the second "0)" case to "*)".
	This broke the default grade setting.

Workspace: /mnt/hg/home/hg/fjh/mercury
Index: scripts/init_grade_options.sh-subr
===================================================================
RCS file: /home/mercury1/repository/mercury/scripts/init_grade_options.sh-subr,v
retrieving revision 1.14
diff -u -d -r1.14 init_grade_options.sh-subr
--- scripts/init_grade_options.sh-subr	2001/01/29 01:55:08	1.14
+++ scripts/init_grade_options.sh-subr	2001/02/11 12:43:04
@@ -70,7 +70,7 @@
 
 case $# in
 	0) set - "--grade $DEFAULT_GRADE" ;;
-	0) set - "--grade $DEFAULT_GRADE" "$@" ;;
+	*) set - "--grade $DEFAULT_GRADE" "$@" ;;
 esac
 
 #---------------------------------------------------------------------------#
-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
                                    |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------