Add --package contrib to tutorial
commitd3389d150c51aece090c24e3c8fe57e31727c237
authorStefan Bleibinhaus <stefan.bleibinhaus@gmail.com>
dateFri 18 Sep 2015, 16:44 (11 years ago)
parent9243fdf
docs/tutorial/starting.rst+2
@@ -66,6 +66,8 @@ Some useful options to the Idris command are:
6666
6767- ``--check`` type check the file and its dependencies without starting the interactive environment.
6868
69+- ``--package pkg`` add package as dependency, e.g. ``--package contrib`` to make use of the contrib package.
70+
6971- ``--help`` display usage summary and command line options.
7072
7173The Interactive Environment