diff options
| author | Pierre Courtieu | 2020-05-28 14:23:17 +0200 |
|---|---|---|
| committer | Pierre Courtieu | 2020-05-28 14:23:17 +0200 |
| commit | 3a5beb79132e23b335f28ab2aef24fa6e587797d (patch) | |
| tree | 0a2b3a10dee2c0e067958926c73db1754c3da935 /pgshell | |
| parent | 5807535598911346f09db0091ccbb2d1c3283433 (diff) | |
Fix default value for proof-shell-last-cmd-left-goals-p.
This variable was still not used anywhere, but will soon.
Diffstat (limited to 'pgshell')
0 files changed, 0 insertions, 0 deletions