Skip to content

Commit

Permalink
Merge pull request #4829 from alexhumphreys/patch-3
Browse files Browse the repository at this point in the history
Update introduction.rst with required `-p` flag
  • Loading branch information
melted committed Mar 17, 2020
2 parents 93cfe98 + 289b058 commit 87577e3
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion docs/effects/introduction.rst
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,8 @@ exceptions, and verified resource management.
This tutorial assumes familiarity with pure programming in Idris,
as described in Sections 1–6 of the main tutorial [1]_. The examples
presented are tested with Idris and can be found in the
examples directory of the Idris repository.
examples directory of the Idris repository. The ``-p effects`` flag
is needed when starting Idris.

Consider, for example, the following introductory function which
illustrates the kind of properties which can be expressed in the type
Expand Down

0 comments on commit 87577e3

Please sign in to comment.