diff options
| author | Christian Grothoff <christian@grothoff.org> | 2020-06-27 18:30:25 +0200 |
|---|---|---|
| committer | Christian Grothoff <christian@grothoff.org> | 2020-07-05 16:50:15 +0200 |
| commit | c88af6df724a47919fd8b0fc1d25f1273120c4e6 (patch) | |
| tree | 91507ce004433b6bf575dcb670dff143888b5971 /doc/.gitignore | |
| parent | 5220e8394f620a05dcc974d6370144980d769070 (diff) | |
fix #6236
Diffstat (limited to 'doc/.gitignore')
0 files changed, 0 insertions, 0 deletions