From 0e864e5e9f803540ba91aa0a5e0c249e2db07164 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 12 Jun 2017 15:42:40 +0200 Subject: [PATCH] chore(doc/bin/README): remove options that no longer exist --- doc/bin/README.md | 25 ------------------------- 1 file changed, 25 deletions(-) diff --git a/doc/bin/README.md b/doc/bin/README.md index 2e05b02c2c..586389e980 100644 --- a/doc/bin/README.md +++ b/doc/bin/README.md @@ -23,28 +23,3 @@ and provides many examples. The tutorial is available in two different forms: - Interactive HTML: http://leanprover.github.io/tutorial/index.html - PDF: http://leanprover.github.io/tutorial/tutorial.pdf - -Command line options --------------------- - -Here are some useful commands for users that do not want to use Emacs, -or prefer command line tools. - -- `-T` do not type check imported .olean files - - % bin/lean -T examples/ex.lean - -The option can save you a significant amount of time if you are importing -many files. Lean still checks the check-sum of the imported files. -So, it still can detect trivial tempering of the .olean files. - -- `-c [file.clean]` create/use a cache file. This option can increase the -compilation time of large files when we are invoking Lean many times -with small incremental changes. - - % bin/lean -c ex.clean examples/ex.lean - -- `--deps` display files imported by a given Lean file. This option -is useful if you want to build your own custom Makefile. - - % bin/lean --deps examples/ex.lean