diff options
| author | Enrico Tassi | 2014-12-17 14:51:29 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-12-17 15:05:05 +0100 |
| commit | f3a6d9080842899e50a44e9474ac0f9a475d5db1 (patch) | |
| tree | 92c11419d7545eb4488b861e888102d990262b3d /dev | |
| parent | df32bf741e872195cc0630088871ccc5bad0906d (diff) | |
Future: blocking by default
This makes queries like Print or Extraction block and not
raise the error "the value is not ready". This should make
CoqIDE work for every kind of script.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions