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 /lib/feedback.mli | |
| parent | dc244adce087f5041ffa94c369b02e538a0a3f4a (diff) | |
| parent | f315ebdd5c7a30284c67e47273eb784dd19b3879 (diff) | |
Merge PR #13250: Micro-optimization in Control.check_for_interrupt.
Reviewed-by: SkySkimmer
Diffstat (limited to 'lib/feedback.mli')
0 files changed, 0 insertions, 0 deletions