diff options
| author | herbelin | 2003-04-29 12:02:24 +0000 |
|---|---|---|
| committer | herbelin | 2003-04-29 12:02:24 +0000 |
| commit | 4b9070eefcdb135226fb4f3c2706519796b0284e (patch) | |
| tree | d850494ca090fbd96850321f16055050b8d36d76 | |
| parent | 9a245295665681af621688ab924093f451ec340c (diff) | |
Moins de ' ' à l'affichage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3973 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/metasyntax.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index ece8acb2b1..51a9eec354 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -336,10 +336,10 @@ let make_hunks etyps symbols from = else UnpTerminal s :: add_break 1 (make NoBreak prods) else - if ws = CanBreak then + if ws = CanBreak or is_ident_tail s.[String.length s - 1] then add_break 1 (UnpTerminal (s^" ") :: make CanBreak prods) else - UnpTerminal (s^" ") :: make CanBreak prods + UnpTerminal s :: make CanBreak prods | Terminal s :: prods -> if is_right_bracket s then |