[m-rev.] for post-commit review: standardize .mih files

[Peter Wang]

On Thu, 01 Jan 2015 22:50:26 +1100 (EST), "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> For review by anyone.
> 
> We discussed the idea earlier, and this mostly implements
> the result of the discussion. The review is mostly for the
> documentation.

I committed this.

Fix indexing of --line-numbers-for-c-headers.

doc/user_guide.texi:
    Do not index --line-numbers-for-c-headers under -n-,
    the short version of --no-line-numbers.

diff --git a/doc/user_guide.texi b/doc/user_guide.texi
index deb7e70..cbea805 100644
--- a/doc/user_guide.texi
+++ b/doc/user_guide.texi
@@ -7221,7 +7221,6 @@ or in Mercury (with @samp{--convert-to-mercury}).
 
 @sp 1
 @item --line-numbers-for-c-headers
- at findex -n-
 @findex --no-line-numbers-for-c-headers
 @findex --line-numbers-for-c-headers
 Put source line numbers in the generated C header files.