aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic
diff options
context:
space:
mode:
authorGravatar Hendrik Tews <hendrik@askra.de>2016-10-28 18:16:28 +0200
committerGravatar Hendrik Tews <hendrik@askra.de>2016-10-28 18:16:28 +0200
commit611e9f557a37364a3de4b89afa336a673dca7cfd (patch)
tree2e86bbb74bd83bfa8d1f578a60a0b9e823393fd7 /generic
parent3b621d71274bc62722876c7229c2e649be6cb378 (diff)
ensure coq-compile-response-buffer is not in a dedicated window
This makes #54 a bit less critical.
Diffstat (limited to 'generic')
0 files changed, 0 insertions, 0 deletions