on master help sign in
Rewrite "mathsing" to "testing"

Looks like global search and replace changed "test" -> "maths" at some point.

commitd03e2b018a05e5a9f9c53f039184627cbdb49811 authorJeremy W. Sherman <jeremyw.sherman@gmail.com> dateTue 28 Jul 2015, 00:29 (11 years ago) parent5339208
1 file changed+3−3
docs/tutorial/packages.rst+3−3
docs/tutorial/packages.rst+3−3
@@ -54,9 +54,9 @@ Given an Idris package file ``maths.ipkg`` it can be used with the Idris compile
5454 package only. This differs from build that type checks **and**
5555 generates code.
5656
57−+ ``idris --mathspkg maths.ipkg`` will compile and run any embedded
58− mathss you have specified in the ``tests`` paramater. More
59− information about mathsing is given in the next section.
57++ ``idris --testpkg maths.ipkg`` will compile and run any embedded
58+ tests you have specified in the ``tests`` paramater. More
59+ information about testing is given in the next section.
6060
6161Once the maths package has been installed, the command line option
6262``--package maths`` makes it accessible (abbreviated to ``-p maths``).