diff options
| author | Enrico Tassi | 2014-12-17 14:18:40 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-12-17 15:05:05 +0100 |
| commit | fac26d37e7e0c9d2d1e3000256ab4641a6c9f95e (patch) | |
| tree | 52980ead9de6ded8701846834019345aff15d220 /kernel/cemitcodes.ml | |
| parent | aaea1138a3a8b90aac0e8f3753a678467af36e72 (diff) | |
CoqIDE: cleanup jobs window on worker death
Diffstat (limited to 'kernel/cemitcodes.ml')
0 files changed, 0 insertions, 0 deletions