diff options
| author | David Aspinall | 2010-08-18 16:19:35 +0000 |
|---|---|---|
| committer | David Aspinall | 2010-08-18 16:19:35 +0000 |
| commit | 14546c942f950b11e1afee9fec396eb21889b75d (patch) | |
| tree | e1ed119c7c6650fed7c5753d8ed39a729b2ffe62 /lib | |
| parent | b087d7665e87d333d6e85ec92b9f161e0368c528 (diff) | |
proof-autosend-loop: don't enter if shell is already busy processing
Diffstat (limited to 'lib')
0 files changed, 0 insertions, 0 deletions