[m-dev.] diff: report error for unknown grade components

[Fergus Henderson]

Estimated hours taken: 0.1

scripts/parse_grade_options.sh-subr:
	Report an error if any of the grade components are unknown.

Workspace: /home/mercury0/fjh/mercury
Index: scripts/parse_grade_options.sh-subr
===================================================================
RCS file: /home/mercury1/repository/mercury/scripts/parse_grade_options.sh-subr,v
retrieving revision 1.14
diff -u -d -r1.14 parse_grade_options.sh-subr
--- scripts/parse_grade_options.sh-subr	2000/02/08 15:32:36	1.14
+++ scripts/parse_grade_options.sh-subr	2000/03/25 07:50:25
@@ -328,6 +328,11 @@
 					stack_trace=true
 					require_tracing=true
 					;;
+				*)
+					echo "$0: unknown grade component" \
+						"\`$grade_piece'" 1>&2
+					exit 1
+					;;
 			esac
 		done
 		;;

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- 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
--------------------------------------------------------------------------