[m-rev.] diff: fix documentation of --feedback-file

[Julien Fischer]

Fix the documentation of --feedback-file.

compiler/options.m:
doc/user_guide.texi:
 	`--feedback-file' requires an argument.

 	Fix a spot where an option name is not quoted /
 	marked up.

Julien.

diff --git a/compiler/options.m b/compiler/options.m
index 94b3568..0121b72 100644
--- a/compiler/options.m
+++ b/compiler/options.m
@@ -5943,9 +5943,9 @@ options_help_misc -->
          "\t(implicit parallelism) using information generated by",
          "\tmdprof_create_feedback.",
          "\tThe profiling feedback file can be specified using the",
-        "\t--feedback file option.",
+        "\t`--feedback-file' option.",

-        "--feedback-file",
+        "--feedback-file <file>",
          "\tUse the specified profiling feedback file which may currently",
          "\tonly be processed for implicit parallelism."
      ]).
diff --git a/doc/user_guide.texi b/doc/user_guide.texi
index a5b5758..7c59f3b 100644
--- a/doc/user_guide.texi
+++ b/doc/user_guide.texi
@@ -10106,10 +10106,10 @@ using the specified distance value.
  Introduce parallel conjunctions where it could be worthwhile (implicit
  parallelism) using deep profiling feedback information generated by
  mdprof_create_feedback. The profiling feedback file can be specified using the
---feedback-file option.
+ at samp{--feedback-file} option.

  @sp 1
- at item --feedback-file
+ at item --feedback-file @var{file}
  @findex --feedback-file
  @cindex Automatic parallelism
  @cindex Profiler feedback