diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-04-06 14:50:04 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-04-06 14:50:04 +0200 |
| commit | e6ae03f3aaf86b08f2da4cd5517ef1a06e87b094 (patch) | |
| tree | a61c736a7f34461506da6c61a50ee80a1b7d854d /plugins/funind | |
| parent | 600c258adee5d6e91e855ff73c58b922d48f444e (diff) | |
| parent | 10e7b9b20319a8c17eb7e3fe8b4516c370470c97 (diff) | |
Merge PR #7178: Fixes issue #7172 (don't include MinGW make in install)
Diffstat (limited to 'plugins/funind')
0 files changed, 0 insertions, 0 deletions