diff options
| author | Pierre-Marie Pédrot | 2014-12-25 15:51:07 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-12-25 16:05:27 +0100 |
| commit | 0e326def6194606d0f1e21daeb45f32e1a061c8f (patch) | |
| tree | b6343d4b7601a7503c1f90e265cd852160304606 /tools | |
| parent | 90ed6636dea41486ddf2cc0daead83f9f0788163 (diff) | |
Inlining Spawn.kill_if in the one place were it was actually used, thus
removing the need of thread creation in the interface.
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/fake_ide.ml | 4 |
1 files changed, 1 insertions, 3 deletions
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 |