diff options
| author | jvoisin | 2022-08-21 15:58:09 +0200 |
|---|---|---|
| committer | jvoisin | 2022-08-21 19:40:17 +0200 |
| commit | e6219a095de78ce03be4a36360020a6f4fe94105 (patch) | |
| tree | 3b5701c88730e914e37ea9d2d966fd2262a63419 /doc/source | |
| parent | b921322ce5faa5c49a14d71bb37f855b0634de0e (diff) | |
Fix sloppy comparison
Diffstat (limited to 'doc/source')
0 files changed, 0 insertions, 0 deletions