Leonardo de Moura dbbacb3bfd chore: remove comment from Linter ... Old frontend is just providing `Syntax.missing`		2020-06-17 21:28:03 -07:00
..
.gitignore	feat: stop compiling Lean code as C++, remove --cpp option	2020-05-14 14:45:33 +02:00
SnakeLinter.lean	chore: remove comment from Linter	2020-06-17 21:28:03 -07:00
SnakeLinter.lean.expected.out	feat: infer module name from cwd instead of LEAN_PATH, also make build system less specific to Init/	2020-05-14 14:38:52 +02:00
test_single.sh	chore: factor out and unify common test behavior; retrieve lean from PATH	2020-05-14 14:38:52 +02:00