diff options
| author | Hendrik Tews | 2017-01-19 11:40:28 +0100 |
|---|---|---|
| committer | Hendrik Tews | 2017-01-19 11:40:28 +0100 |
| commit | 4bcac92df46da9e68b5e3d565bb118fb63b4feb4 (patch) | |
| tree | ec19916cf72884ee83fc7f52d8c7d87b83ce767f /pgshell | |
| parent | 77c3f2eac868f177b73d2aa59b277e40fc48fd0c (diff) | |
save settings not defined with defpacustom (fixes #142)
- infrastructure for saving/resetting customizations not defined
with defpacustom
- improve Coq -> Auto Compilation menu
- polish documentation and manual
Diffstat (limited to 'pgshell')
0 files changed, 0 insertions, 0 deletions