diff options
| author | herbelin | 2009-09-15 19:11:44 +0000 |
|---|---|---|
| committer | herbelin | 2009-09-15 19:11:44 +0000 |
| commit | acefca3c863d5c022214deb3bbd685baec86421e (patch) | |
| tree | 8ee5cde1a07e55cd878c6ad8facebde8b39e8673 | |
| parent | 4f2d820de5586a657d11e61377c3bdb82fcd5eeb (diff) | |
Fixed compilation error message which was no longer emacs-compliant since
revision 11316.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12331 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/toplevel.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index a043c404b4..54e491f906 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -176,11 +176,10 @@ let print_location_in_file s inlibrary fname loc = try let (line, bol) = line_of_pos 1 0 0 in close_in ic; - hov 0 - (errstrm ++ str"File " ++ str ("\""^fname^"\"") ++ str"," ++ spc() ++ - hov 0 (str"line " ++ int line ++ str"," ++ spc() ++ - str"characters " ++ - Cerrors.print_loc (make_loc (bp-bol,ep-bol))) ++ str":") ++ + hov 0 (* No line break so as to follow emacs error message format *) + (errstrm ++ str"File " ++ str ("\""^fname^"\"") ++ + str", line " ++ int line ++ str", characters " ++ + Cerrors.print_loc (make_loc (bp-bol,ep-bol))) ++ str":" ++ fnl () with e -> (close_in ic; |