diff options
| author | Pierre-Marie Pédrot | 2014-07-21 17:50:47 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-07-21 17:50:47 +0200 |
| commit | 441a23b293da55ce01bb7406ec2f78e0f59b3f1e (patch) | |
| tree | 4f124d3481e5365b105602b5c19559334a90306e | |
| parent | 9b6c7b1a50a4ea87877017848b0f6b20c582cf87 (diff) | |
Missing space in pretty-printer
| -rw-r--r-- | printing/prettyp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 67b3df35e0..03ad7889fa 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -375,7 +375,7 @@ let print_located_qualid name flags ref = if DirPath.is_empty dir then str ("No " ^ name ^ " of basename") ++ spc () ++ pr_id id else - str ("No " ^ name ^ " of suffix") ++ pr_qualid qid + str ("No " ^ name ^ " of suffix") ++ spc () ++ pr_qualid qid | l -> prlist_with_sep fnl (fun (o,oqid) -> |