diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-04-05 17:31:47 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-04-05 17:31:47 +0200 |
| commit | e720740bfa36e941a77fdc29c659dbe5a66b6fa4 (patch) | |
| tree | ce9407e145b56e6a31ba28f0b35681bf665ecc21 /lib | |
| parent | 332efef9073eadb4907cd4e9ee1ba17bcc16afc6 (diff) | |
Fix #5981, bugs/opened/3263.v is non-deterministic by removing the test.
Since this is an open bug, it is of lesser importance but
non-deterministic tests are a real problem OTOH.
Diffstat (limited to 'lib')
0 files changed, 0 insertions, 0 deletions