diff options
Diffstat (limited to 'lib/Printlines.ml')
-rw-r--r-- | lib/Printlines.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/lib/Printlines.ml b/lib/Printlines.ml index b60fdf4a..b270e229 100644 --- a/lib/Printlines.ml +++ b/lib/Printlines.ml @@ -101,11 +101,13 @@ let copy oc pref b first last = try while b.lineno <= last do let c = input_char b.chan in - output_char oc c; - if c = '\n' then begin + match c with + | '\n' -> + output_char oc c; b.lineno <- b.lineno + 1; if b.lineno <= last then output_string oc pref - end + | '\r' | '\011' | '\012' -> output_char oc ' ' + | _ -> output_char oc c done with End_of_file -> output_char oc '\n' |