diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-10-15 08:10:05 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-10-15 08:10:05 +0200 |
| commit | 7402a7788b6a73bd5c0cb9078823d48e6f01a357 (patch) | |
| tree | 6a73c871455c18c17e52752bef2fb81fbd2b18be /ide/wg_ScriptView.ml | |
| parent | 1d6c4f135d42a008b21d86d8ecd8b329405d8d7c (diff) | |
Fix detection of ties in oracle_order.
This commit has no impact, since l2r is always false in practice due to
the definition of default_conv.
Diffstat (limited to 'ide/wg_ScriptView.ml')
0 files changed, 0 insertions, 0 deletions