aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-12-14 13:25:27 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-12-14 13:25:27 +0100
commitd3c91b093c8adeba2225e453f50a9936e1adb012 (patch)
tree6492ade006d756eb9c93f45e8f925e4313c46fec
parent180af0dde65e4532cdeb13ec9aa43d8e83f7408f (diff)
Revert "Fixing bug #3817."
-rw-r--r--ide/ide_slave.ml14
1 files changed, 2 insertions, 12 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 62e1bad43..b4757c8f7 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -451,18 +451,8 @@ let loop () =
let in_ch, out_ch = Spawned.get_channels () in
let xml_oc = Xml_printer.make (Xml_printer.TChannel out_ch) in
CThread.prepare_in_channel_for_thread_friendly_io in_ch;
- let safe_read s len =
- (** Ignore interrupt when reading a stanza *)
- let _ = Unix.sigprocmask Unix.SIG_BLOCK [Sys.sigint] in
- try
- let ans = CThread.thread_friendly_read in_ch s ~off:0 ~len in
- let _ = Unix.sigprocmask Unix.SIG_UNBLOCK [Sys.sigint] in
- ans
- with e ->
- let _ = Unix.sigprocmask Unix.SIG_UNBLOCK [Sys.sigint] in
- raise e
- in
- let in_lb = Lexing.from_function safe_read in
+ let in_lb = Lexing.from_function (fun s len ->
+ CThread.thread_friendly_read in_ch s ~off:0 ~len) in
let xml_ic = Xml_parser.make (Xml_parser.SLexbuf in_lb) in
let () = Xml_parser.check_eof xml_ic false in
set_logger (slave_logger xml_oc);