diff options
| author | coqbot-app[bot] | 2020-11-04 15:49:27 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-04 15:49:27 +0000 |
| commit | 4f8e14a8026f01e1dcc1b8929645858d2bbb504e (patch) | |
| tree | 7763c988adc4a2f9b1a701c4c01eedf409f384ef | |
| parent | 5a25287987b8683ee3cbaa9a87ba0f8aebba896b (diff) | |
| parent | 2812f8323e46e22ccde1606c71d908059b732e44 (diff) | |
Merge PR #13302: Fix test-suite in async mode.
Reviewed-by: SkySkimmer
| -rw-r--r-- | test-suite/output/ErrorLocation_13241_1.v | 1 | ||||
| -rw-r--r-- | test-suite/output/ErrorLocation_13241_2.v | 1 |
2 files changed, 2 insertions, 0 deletions
diff --git a/test-suite/output/ErrorLocation_13241_1.v b/test-suite/output/ErrorLocation_13241_1.v index ff92085133..3102b13fb8 100644 --- a/test-suite/output/ErrorLocation_13241_1.v +++ b/test-suite/output/ErrorLocation_13241_1.v @@ -2,3 +2,4 @@ Ltac a := intro. Ltac b := a. Goal True. b. +Abort. diff --git a/test-suite/output/ErrorLocation_13241_2.v b/test-suite/output/ErrorLocation_13241_2.v index 280d4a3506..b82f36ed6f 100644 --- a/test-suite/output/ErrorLocation_13241_2.v +++ b/test-suite/output/ErrorLocation_13241_2.v @@ -2,3 +2,4 @@ Ltac a _ := intro. Ltac b := a (). Goal True. b. +Abort. |