diff options
author | 2018-04-25 11:49:03 +0200 | |
---|---|---|
committer | 2018-05-03 14:44:13 +0200 | |
commit | 4aabbce60f777ecfb2761954e177f161fc9042ff (patch) | |
tree | 538ff40f5d792905054e641af4942bbb38a5d65d /library/nametab.mli | |
parent | fad6eee8ddb28fa7840044c65aa02557285e23f0 (diff) |
Fixes issue #7081 / Windows build: strip in lablgtk build can fail randomly
Diffstat (limited to 'library/nametab.mli')
0 files changed, 0 insertions, 0 deletions