diff --git a/doc/fixing_tests.md b/doc/fixing_tests.md index df3d5d4be..84f5fcbb4 100644 --- a/doc/fixing_tests.md +++ b/doc/fixing_tests.md @@ -29,3 +29,13 @@ executing When the `yes` option is provided, `meld` is automatically invoked whenever there is discrepancy between the produced and expected outputs. `meld` can also be used to repair the problems. + +Here is the list of directories where produced output is compared with +the expected output (stored in a `*.expected.out` file). + +- [`tests/lean`](../tests/lean) +- [`tests/lean/interactive`](../tests/lean/interactive) + +Remark: in the directory `tests/lean/interactive`, the input test files have extension `.input`. +They simulate commands sent from Emacs to Lean. +The `.lean` files in this directory are used to simulate files opened by the user. \ No newline at end of file