diff options
| author | coqbot-app[bot] | 2020-11-02 13:26:10 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-02 13:26:10 +0000 |
| commit | dfdecf24210ee287d554cf4296bd0ccfffe310d8 (patch) | |
| tree | 9c7f36af133e94918776de4392270623364c8f8e | |
| parent | dc244adce087f5041ffa94c369b02e538a0a3f4a (diff) | |
| parent | f315ebdd5c7a30284c67e47273eb784dd19b3879 (diff) | |
Merge PR #13250: Micro-optimization in Control.check_for_interrupt.
Reviewed-by: SkySkimmer
| -rw-r--r-- | lib/control.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/lib/control.ml b/lib/control.ml index bb42b5727e..95ea3935a7 100644 --- a/lib/control.ml +++ b/lib/control.ml @@ -18,10 +18,12 @@ let enable_thread_delay = ref false let check_for_interrupt () = if !interrupt then begin interrupt := false; raise Sys.Break end; - incr steps; - if !enable_thread_delay && !steps = 1000 then begin - Thread.delay 0.001; - steps := 0; + if !enable_thread_delay then begin + incr steps; + if !steps = 1000 then begin + Thread.delay 0.001; + steps := 0; + end end (** This function does not work on windows, sigh... *) |
