idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-19 01:01:59 +03:00
Code Issues Projects Releases Wiki Activity

Cleaning up unnecessary code.

Browse Source
This commit is contained in:
Matthew-Mosior 2024-08-04 21:43:16 -04:00
parent d788e07c32
commit 77d4780985
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/Idris/Package.idr
View File

@ -845,8 +845,8 @@ clean pkg opts -- `opts` is not used but might be in the future
(executable pkg) (executable pkg)
-- clean out the generated docs -- clean out the generated docs
let build = build_dir (dirs (options defs)) let build = build_dir (dirs (options defs))
() <- deleteDocsFolder $ build </> "docs" </> "docs" deleteDocsFolder $ build </> "docs" </> "docs"
() <- deleteDocsFolder $ build </> "docs" deleteDocsFolder $ build </> "docs"
runScript (postclean pkg) runScript (postclean pkg)
where where
delete : String -> Core () delete : String -> Core ()