aboutsummaryrefslogtreecommitdiff
path: root/lib/control.ml
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-11-02 13:26:10 +0000
committerGitHub2020-11-02 13:26:10 +0000
commitdfdecf24210ee287d554cf4296bd0ccfffe310d8 (patch)
tree9c7f36af133e94918776de4392270623364c8f8e /lib/control.ml
parentdc244adce087f5041ffa94c369b02e538a0a3f4a (diff)
parentf315ebdd5c7a30284c67e47273eb784dd19b3879 (diff)
Merge PR #13250: Micro-optimization in Control.check_for_interrupt.
Reviewed-by: SkySkimmer
Diffstat (limited to 'lib/control.ml')
-rw-r--r--lib/control.ml10
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... *)