diff options
| author | Thomas Kleymann | 1998-11-02 17:17:52 +0000 |
|---|---|---|
| committer | Thomas Kleymann | 1998-11-02 17:17:52 +0000 |
| commit | da2ed54dac8160ae4cdb25c8e048600dc1e38973 (patch) | |
| tree | 1280a9705bfc915ce53a753cd9f95cfb8508e9a6 /html | |
| parent | 722f150e05ae402a1195fa2c12b8206a433b0771 (diff) | |
Proof General no longer changes selected window/buffer under your feet.
Diffstat (limited to 'html')
0 files changed, 0 insertions, 0 deletions