diff options
| author | Pierre-Marie Pédrot | 2020-08-27 17:01:59 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-27 17:01:59 +0200 |
| commit | dac417a38dee2ce5800e8f66406bd08838535dc0 (patch) | |
| tree | dc699d8fea49b21379c643a0810a7770f9120715 /stm | |
| parent | 1abf7c94f97948f8171c2fe1fec99cd890e8d1f6 (diff) | |
Fix .gitignore after the merge of #12849.
A stray generated file was forgotten.
Diffstat (limited to 'stm')
0 files changed, 0 insertions, 0 deletions