diff options
| author | Guillaume Melquiond | 2014-03-04 18:17:12 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2014-03-04 18:17:24 +0100 |
| commit | fe9e7e09329ad78582e46fb0441e403de8b98547 (patch) | |
| tree | cc0a4b86fb0e793c8c275ecf7654c44a2d086813 /pretyping/pretype_errors.mli | |
| parent | b0dc4e0291774f39a6e76e1f09cacc47986cd4a1 (diff) | |
Move error and job display to the lower right pane.
Diffstat (limited to 'pretyping/pretype_errors.mli')
0 files changed, 0 insertions, 0 deletions