diff options
| author | Enrico Tassi | 2018-10-08 10:29:58 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-10-08 10:29:58 +0200 |
| commit | 39248aecd9211dde66d80b312b5b66c8fd45cfa4 (patch) | |
| tree | c00056e19b05bffb4243b81cdcf61b0e3132ae6b /dev | |
| parent | cbbd19eb3d9740063e900463f6406ba0a144c96a (diff) | |
| parent | d19372209eca556bb07116b518d8740ff6385035 (diff) | |
Merge PR #8630: Some cleaning in the test suite
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/tools/update-compat.py | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/tools/update-compat.py b/dev/tools/update-compat.py index 7c8b9f025c..14094553a2 100755 --- a/dev/tools/update-compat.py +++ b/dev/tools/update-compat.py @@ -17,7 +17,7 @@ FLAGS_ML_PATH = os.path.join(ROOT_PATH, 'lib', 'flags.ml') COQARGS_ML_PATH = os.path.join(ROOT_PATH, 'toplevel', 'coqargs.ml') G_VERNAC_PATH = os.path.join(ROOT_PATH, 'vernac', 'g_vernac.mlg') DOC_INDEX_PATH = os.path.join(ROOT_PATH, 'doc', 'stdlib', 'index-list.html.template') -BUG_4798_PATH = os.path.join(ROOT_PATH, 'test-suite', 'bugs', 'closed', '4798.v') +BUG_4798_PATH = os.path.join(ROOT_PATH, 'test-suite', 'bugs', 'closed', 'bug_4798.v') TEST_SUITE_PATHS = tuple(os.path.join(ROOT_PATH, 'test-suite', 'success', i) for i in ('CompatOldOldFlag.v', 'CompatOldFlag.v', 'CompatPreviousFlag.v', 'CompatCurrentFlag.v')) TEST_SUITE_DESCRIPTIONS = ('current-minus-three', 'current-minus-two', 'current-minus-one', 'current') |