Merge pull request #4397 from GuiltyDolphin/gd/fix-package-name-typo
Fix typo in package name
commit24d186742d95c792f6906f84aec8ace9fe57e500
authorNiklas Larsson <metaniklas@gmail.com>
dateThu 29 Mar 2018, 15:40 (9 years ago)
parent3e9de43a7d3c09
docs/reference/packages.rst+1−1
@@ -123,7 +123,7 @@ Package files support comments using the standard Idris singleline ``--`` and mu
123123Using Package files
124124===================
125125
126−Given an Idris package file ``text.ipkg`` it can be used with the Idris compiler as follows:
126+Given an Idris package file ``test.ipkg`` it can be used with the Idris compiler as follows:
127127
128128+ ``idris --build test.ipkg`` will build all modules in the package
129129