diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-05-31 15:15:32 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-05-31 15:15:32 +0200 |
| commit | 88a632b508977966b1e8d4f4449824a55ffc65d1 (patch) | |
| tree | 793d2274b8a9bf72be57dd3296b69f0c9eaba21c /.github | |
| parent | ac8a84e3b4dc530b000e17b72c7e26f7a957420f (diff) | |
| parent | 3ce7ae5c2de955d5d79fc23a02ee06fa9071f24a (diff) | |
Merge PR #7401: Automatically run alienclean before compiling.
Diffstat (limited to '.github')
0 files changed, 0 insertions, 0 deletions