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

Removing unnecessary line.

Browse Source
This commit is contained in:
Matthew-Mosior 2024-07-25 14:14:13 -04:00
parent 2d4e7ad825
commit f510501386
1 changed files with 0 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/Idris/Package.idr
View File

@ -844,7 +844,6 @@ clean pkg opts -- `opts` is not used but might be in the future
maybe (pure ()) (\e => delete (outputdir </> e)) maybe (pure ()) (\e => delete (outputdir </> e))
(executable pkg) (executable pkg)
-- clean out the generated docs -- clean out the generated docs
defs <- get Ctxt
let build = build_dir (dirs (options defs)) let build = build_dir (dirs (options defs))
let docBase = build </> "docs" let docBase = build </> "docs"
let docDir = docBase </> "docs" let docDir = docBase </> "docs"