diff options
| author | Pierre-Marie Pédrot | 2020-10-22 17:25:20 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-10-22 17:25:20 +0200 |
| commit | f315ebdd5c7a30284c67e47273eb784dd19b3879 (patch) | |
| tree | fa4cd40d9fbd464b5f75f9d76e9fe0676fa6cbfa /lib/objFile.ml | |
| parent | fe095cd8b63e363e82953503cb84a851296c1965 (diff) | |
Micro-optimization in Control.check_for_interrupt.
We do not have to increase the step counter when out of the threaded mode since
this counter is only relevant when in that mode.
Diffstat (limited to 'lib/objFile.ml')
0 files changed, 0 insertions, 0 deletions