mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-18 08:42:11 +03:00
Remove unnecessary whitespace.
This commit is contained in:
parent
ccff608e19
commit
063f353a10
@ -862,7 +862,7 @@ clean pkg opts -- `opts` is not used but might be in the future
|
||||
= do let ttFile = builddir </> joinPath ns </> mod
|
||||
delete $ ttFile <.> "ttc"
|
||||
delete $ ttFile <.> "ttm"
|
||||
|
||||
|
||||
deleteDocBaseFolder : String -> Core ()
|
||||
deleteDocBaseFolder build
|
||||
= do let docBase = build </> "docs"
|
||||
|
Loading…
Reference in New Issue
Block a user