diff options
| author | Enrico Tassi | 2014-09-08 13:15:58 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2014-09-09 13:11:38 +0200 |
| commit | de5ed8e17df8433d4f0ffe6a6440505b5a530638 (patch) | |
| tree | 8660ea9edb389bd60a1beb98f7b11192c55c33a3 /stm/asyncTaskQueue.ml | |
| parent | 4d601a87b775529b7d516fa213c688b6ecf5246d (diff) | |
IDE: disable editable text area underline when -debug
This way a user *can* use coqide with -debug
Diffstat (limited to 'stm/asyncTaskQueue.ml')
0 files changed, 0 insertions, 0 deletions