improved gdoc output for function parameters.

diff --git a/doc/scripts/gdoc b/doc/scripts/gdoc
index be0621af529af9c55a53639a3771ccc3eaf08fb4..ea798b9fccd008d04847adad63550e55a8d704d9 100755 (executable)
--- a/doc/scripts/gdoc
+++ b/doc/scripts/gdoc
@@ -151,10 +151,10 @@ $type_env = "(\\\$[A-Za-z0-9_]+)";
                     $type_param, '" <tt><b>$1</b></tt>"' );
 $blankline_html = "<p>";
 
-%highlights_texinfo = ( $type_param, '" \@code{$1}"',
-                       $type_constant, '"\@code{$1}"',
-                       $type_func, '"\@code{$1}"',
-                       $type_struct, '"\@code{$1}"',
+%highlights_texinfo = ( $type_param, '" \@code{$1} "',
+                       $type_constant, '"\@code{$1} "',
+                       $type_func, '"\@code{$1} "',
+                       $type_struct, '"\@code{$1} "',
                         );
 $blankline_texinfo = "";