Merge pull request #3421 from jfdm/doc-fix
Fixed heading issue in docs.
commit62751fa51ec18fab2fc4ef581577ad4aa9700ed2
authorJan de Muijnck-Hughes <jfdm@users.noreply.github.com>
dateMon 12 Sep 2016, 09:32 (10 years ago)
parentf852094e7b4da5
docs/reference/internals.rst+4
@@ -1,3 +1,7 @@
1+*****************
2+Idris' Internals
3+*****************
4+
15Note: this is still a fairly raw set of notes taken by David
26Christiansen at Edwin's presentation at the 2013 Idris Developers
37Meeting. They're in the process of turning into a useful guide - feel