diff options
| author | Erik Martin-Dorel | 2017-01-13 08:42:13 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2017-01-13 08:42:34 +0100 |
| commit | 9568a34f665a6f3dca06271ffd6e914d9bd2a5ad (patch) | |
| tree | 248d6f7503ccf13e819d484309f7c318aea223cf /kernel | |
| parent | aa21c209f85f37b3d16ff499bbeac15e967bf78f (diff) | |
Properly remove aux files in subdirectories (bug #5089).
The aux file for foo/bar.v is foo/.bar.aux, not .foo/bar.aux.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions