[m-dev.] diff: allow -H option in scripts/*

[Fergus Henderson]

Estimated hours taken: 0.25

scripts/parse_grade_options.sh-subr:
	Allow `-H' as a synomym for `--high-level-code',
	to match the behaviour of mmc.

Workspace: /home/pgrad/fjh/ws/hg
Index: scripts/parse_grade_options.sh-subr
===================================================================
RCS file: /home/mercury1/repository/mercury/scripts/parse_grade_options.sh-subr,v
retrieving revision 1.15
diff -u -d -r1.15 parse_grade_options.sh-subr
--- scripts/parse_grade_options.sh-subr	2000/03/25 08:14:42	1.15
+++ scripts/parse_grade_options.sh-subr	2000/05/24 04:58:11
@@ -19,9 +19,9 @@
 #
 #---------------------------------------------------------------------------#
 
-	--high-level-code)
+	--high-level-code|-H)
 		highlevel_code=true ;;
-	--no-high-level-code)
+	--no-high-level-code|-H-)
 		highlevel_code=false ;;
 
 	--high-level-data)

-- 
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
--------------------------------------------------------------------------