diff options
| author | Christian Grothoff <christian@grothoff.org> | 2018-01-04 11:55:00 +0100 |
|---|---|---|
| committer | Christian Grothoff <christian@grothoff.org> | 2018-01-04 11:55:00 +0100 |
| commit | 23cb23b1e73f996fddf3a1cbb22329c4dcf632e9 (patch) | |
| tree | e7a2cb0f015dc3b5a15e9d82b3a0b50194911a34 /doc/.gitignore | |
| parent | 77a58673ef432296c0ac9a8778cadfb6d5982061 (diff) | |
fix minor formatting issue
Diffstat (limited to 'doc/.gitignore')
0 files changed, 0 insertions, 0 deletions