mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-08-16 12:10:39 +03:00
Fixed typo
This commit is contained in:
parent
0380bb9978
commit
83e4fa5c12
@ -76,7 +76,7 @@ Extra-doc-files:
|
||||
samples/tutorial/*.idr
|
||||
samples/ST/*.idr
|
||||
samples/ST/Graphics/*.idr
|
||||
samples/ST/NET/*.idr
|
||||
samples/ST/Net/*.idr
|
||||
samples/misc/*.lidr
|
||||
|
||||
-- extra-source-files is generated by Setup.hs using `git --ls-files`.
|
||||
|
Loading…
Reference in New Issue
Block a user