diff options
Diffstat (limited to 'testsuite/tests/memory-model/publish.ml')
-rw-r--r-- | testsuite/tests/memory-model/publish.ml | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/testsuite/tests/memory-model/publish.ml b/testsuite/tests/memory-model/publish.ml index 7f778307a1..e5750d3636 100644 --- a/testsuite/tests/memory-model/publish.ml +++ b/testsuite/tests/memory-model/publish.ml @@ -1,9 +1,12 @@ (* TEST - modules="opt.ml barrier.ml hist.ml shared.ml run.ml outcome.ml" - * not-bsd - ** not-windows - *** bytecode - ** native + modules = "opt.ml barrier.ml hist.ml shared.ml run.ml outcome.ml"; + not-bsd; + { + not-windows; + bytecode; + }{ + native; + } *) (* Memory model: test the _publish idiom *) |