diff options
| author | Erik Martin-Dorel | 2018-08-25 18:27:09 +0200 |
|---|---|---|
| committer | GitHub | 2018-08-25 18:27:09 +0200 |
| commit | 69066bf2cb97d6df74a069c3e90155e43353a2a0 (patch) | |
| tree | c9ffccbd8bb3ff4d16f6634c3c438990b96ce23d /pgshell | |
| parent | 95786256fc32ad6881b4d95d98b5b41acd171fc9 (diff) | |
| parent | 7b10643f60e4db501a40f1cf84f42810320121be (diff) | |
Merge pull request #169 from ProofGeneral/help-span-extended
Fix #158 by extending helpspan
Diffstat (limited to 'pgshell')
0 files changed, 0 insertions, 0 deletions