From 92579449f62f0fd7699b0b447f3aee0d82d1b5c3 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 23 Feb 2017 13:48:47 +0100 Subject: [safe-string] tools No functional changes. --- tools/coqworkmgr.ml | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) (limited to 'tools/coqworkmgr.ml') diff --git a/tools/coqworkmgr.ml b/tools/coqworkmgr.ml index d7bdf907a..b8e69d6c6 100644 --- a/tools/coqworkmgr.ml +++ b/tools/coqworkmgr.ml @@ -72,10 +72,13 @@ let really_read_fd fd s off len = let raw_input_line fd = try let b = Buffer.create 80 in - let s = String.make 1 '\000' in - while s <> "\n" do + let s = Bytes.make 1 '\000' in + let endl = Bytes.of_string "\n" in + let endr = Bytes.of_string "\r" in + while Bytes.compare s endl <> 0 do really_read_fd fd s 0 1; - if s <> "\n" && s <> "\r" then Buffer.add_string b s; + if Bytes.compare s endl <> 0 && Bytes.compare s endr <> 0 + then Buffer.add_bytes b s; done; Buffer.contents b with Unix.Unix_error _ -> raise End_of_file -- cgit v1.2.3