Skip to content
This repository was archived by the owner on Nov 12, 2025. It is now read-only.

Correct minor typo in documentation#4919

Open
isti115 wants to merge 1 commit into
idris-lang:masterfrom
isti115:patch-1
Open

Correct minor typo in documentation#4919
isti115 wants to merge 1 commit into
idris-lang:masterfrom
isti115:patch-1

Conversation

@isti115

@isti115 isti115 commented May 23, 2022

Copy link
Copy Markdown

No description provided.

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant