diff options
| author | Gaëtan Gilbert | 2019-05-22 13:52:13 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-05-22 13:52:13 +0200 |
| commit | 2ba0994e11b3cebf4d33c5712f873998ad5ddd7b (patch) | |
| tree | 8306ea1dc70d7ce9360e28715866f7772d97dee0 /dev | |
| parent | e7d03413c6b8f8fbcc537a43da4c3f9ff19007ad (diff) | |
Fix #10208 don't fail when passed extensionless -topfile
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions