From 0e326def6194606d0f1e21daeb45f32e1a061c8f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 25 Dec 2014 15:51:07 +0100
Subject: Inlining Spawn.kill_if in the one place were it was actually used,
 thus removing the need of thread creation in the interface.

---
 tools/fake_ide.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'tools')

diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index df114d059a..47782db080 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -289,9 +289,7 @@ let usage () =
      (Filename.basename Sys.argv.(0))
      (Parser.print grammar))
 
-module Coqide = Spawn.Sync(struct
-  let add_timeout ~sec:_ _ = ()
-end)
+module Coqide = Spawn.Sync(struct end)
 
 let main =
   Sys.set_signal Sys.sigpipe
-- 
cgit v1.2.3