[m-rev.] diff: remove line from user guide that shouldn't be there.

[Ian MacLarty]

Estimated hours taken: 0.1
Branches: main

Remove line that shouldn't be in user_guide.texi.

doc/user_guide.texi
	Remove line "on" that shouldn't be there.

Index: doc/user_guide.texi
===================================================================
RCS file: /home/mercury1/repository/mercury/doc/user_guide.texi,v
retrieving revision 1.400
diff -u -r1.400 user_guide.texi
--- doc/user_guide.texi	11 Dec 2004 01:59:50 -0000	1.400
+++ doc/user_guide.texi	13 Dec 2004 01:56:27 -0000
@@ -2728,7 +2728,6 @@
 @item
 @samp{xml_tmp_filename} is the name of the file to dump XML to before
 invoking your XML browser.
-on 
 @sp 1
 @item
 @samp{xml_browser_cmd} is the shell command(s) used to invoke your XML browser.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------