idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-24 06:52:19 +03:00
Code Issues Projects Releases Wiki Activity

Added notes: :exec needs to be passed main (#2946)

Browse Source
This commit is contained in:
Marshall Abrams 2023-04-16 02:10:08 -05:00 committed by GitHub
parent 9544162bc4
commit 3eeb4f4cd3
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 3 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
docs/source/typedd/typedd.rst
View File

@ -19,7 +19,7 @@ necessary changes.
Chapter 1
---------
No changes necessary
Instead of entering ``:exec`` to run ``Hello.idr`` in the REPL, enter ``:exec main``.
Chapter 2
---------
@ -40,6 +40,8 @@ In ``AveMain.idr`` and ``Reverse.idr`` add:
import System.REPL -- for 'repl'
Instead of entering ``:exec`` to run ``main`` from ``AveMain.idr``, enter ``:exec main``.
Chapter 3
---------