diff options
| author | Gaëtan Gilbert | 2019-04-06 14:32:30 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-04-06 14:32:30 +0200 |
| commit | 1daace521f04bf95eee77a6fcf3e15d067520e70 (patch) | |
| tree | 3661f9f24030ff75004c8d47710206ad0a12d805 /dev/include_dune | |
| parent | 5b2005d7224c2e9037e7e235e643602ac9b8481a (diff) | |
Fix numeral notations test in async mode.
Async causes output reordering in one test. Since we don't care about
the output of that test (it's just a [Fail]) we move it to success/.
Diffstat (limited to 'dev/include_dune')
0 files changed, 0 insertions, 0 deletions