diff options
| author | Enrico Tassi | 2019-12-11 15:47:25 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-12-11 15:47:25 +0100 |
| commit | 4a7a5c36802701d0e1b47956bb14cfc9cab99baa (patch) | |
| tree | 8b0c59b14cd2c2766c0f4d4b7972c079de8029e5 /tools | |
| parent | 9522f39615e7f20c2ce4e1d4274ef475fdcca26e (diff) | |
| parent | c3266d737bbda2b707ba1f2f78ecfe4e2e9f9ab8 (diff) | |
Merge PR #11201: remove *.vos and *.vok file in "make clean"
Reviewed-by: gares
Diffstat (limited to 'tools')
0 files changed, 0 insertions, 0 deletions