git.iko.soy/Idris-dev
on master help sign in
Add --package contrib to tutorial
d3389d1Stefan Bleibinhaus
docs/tutorial/starting.rst+2
compare with master
unifiedsplit
@@ -66,6 +66,8 @@ Some useful options to the Idris command are:
66
66
67- ``--check`` type check the file and its dependencies without starting the interactive environment.
67- ``--check`` type check the file and its dependencies without starting the interactive environment.
68
68
69+- ``--package pkg`` add package as dependency, e.g. ``--package contrib`` to make use of the contrib package.
70+
69- ``--help`` display usage summary and command line options.
71- ``--help`` display usage summary and command line options.
70
72
71The Interactive Environment
73The Interactive Environment