Correct minor typo in documentation#4919

isti115 wants to merge 1 commit into

idris-lang:masteridris-lang/Idris-dev:masterfrom

isti115:patch-1isti115/Idris-dev:patch-1Copy head branch name to clipboard