aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2014-03-04 18:17:12 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2014-03-04 18:17:24 +0100
commitfe9e7e09329ad78582e46fb0441e403de8b98547 (patch)
treecc0a4b86fb0e793c8c275ecf7654c44a2d086813 /tactics
parentb0dc4e0291774f39a6e76e1f09cacc47986cd4a1 (diff)
Move error and job display to the lower right pane.
Diffstat (limited to 'tactics')
0 files changed, 0 insertions, 0 deletions