diff options
| author | Maxime Dénès | 2017-09-22 11:46:33 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-09-22 11:46:33 +0200 |
| commit | 06a723190858da8ed3f30736f22398aa7822c959 (patch) | |
| tree | 805ad45a4492a880dbf6008906eeaff807388ad0 /ide/ide_slave.ml | |
| parent | 63b3b3f307053fd055355d8a669456c988d083aa (diff) | |
| parent | 569e8f7601ee1484f8373320a102fa2ab026078c (diff) | |
Merge PR #1055: Remove STM vernaculars
Diffstat (limited to 'ide/ide_slave.ml')
| -rw-r--r-- | ide/ide_slave.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index b11a11606f..f00b1e1421 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -413,6 +413,7 @@ let eval_call c = Interface.quit = (fun () -> quit := true); Interface.init = interruptible init; Interface.about = interruptible about; + Interface.wait = interruptible Stm.wait; Interface.interp = interruptible interp; Interface.handle_exn = handle_exn; Interface.stop_worker = Stm.stop_worker; |