[m-rev.] diff: add option --mercury-standard-library-directory

[Simon Taylor]

Estimated hours taken: 0.1
Branches: main

compiler/options.m:
	Fix a typo in my last change.
 					% The mmc script will set the default
	-				% --mercury_standard_library_directory.
	+				% standard library directory.

Index: options.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/options.m,v
retrieving revision 1.345
diff -u -u -r1.345 options.m
--- options.m	11 Nov 2001 10:10:17 -0000	1.345
+++ options.m	11 Nov 2001 10:11:30 -0000
@@ -941,7 +941,7 @@
 	mercury_library_special -	string_special,
 	mercury_libraries -		accumulating([]),
 					% The mmc script will set the default
-					% --mercury_standard_library_directory.
+					% standard library directory.
 	mercury_standard_library_directory - maybe_string(no),
 	init_file_directories -		accumulating([]),
 	init_files -			accumulating([]),
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------