diff options
| author | Christian Grothoff <christian@grothoff.org> | 2022-09-20 23:18:46 +0200 |
|---|---|---|
| committer | Christian Grothoff <christian@grothoff.org> | 2022-09-20 23:18:46 +0200 |
| commit | a2c179373e9493506cbae5a6a51c015f0403b662 (patch) | |
| tree | 0df8b80b735877f5caa645b0ec1dda39dc47ba72 /.gitignore | |
| parent | bf85d6f3d14bf510f23b4cef5414e2219bb3c91d (diff) | |
-fix issue on Florian's system
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions