diff options
| author | Gaëtan Gilbert | 2017-11-24 11:02:02 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2017-11-28 12:31:04 +0100 |
| commit | 797736bbd7975926cc028a9f7c9c577e9c1e476b (patch) | |
| tree | 551f4a6b277b0cb976b53032748ffec44d35c509 /dev/base_include | |
| parent | f303ed9fb26797b9ec7d172fe583e7ee607ae441 (diff) | |
Make the micromega extraction check a regular output test.
This allows us to enforce that it works without breaking the build
when it doesn't.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions