From daf27fd1947a9318e20aad8970268823232a6690 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 25 Feb 2015 11:46:10 -0800 Subject: [PATCH] doc(fixing_tests): add links to directories containing tests that compare produced vs expected output --- doc/fixing_tests.md | 10 ++++++++++ 1 file changed, 10 insertions(+) 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