mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-19 09:12:34 +03:00
Adding files to address --clean does not remove the generated docs sub issue of issue 1918.
This commit is contained in:
parent
91d0eb3e31
commit
2d4e7ad825
@ -843,6 +843,21 @@ clean pkg opts -- `opts` is not used but might be in the future
|
|||||||
deleteFolder builddir []
|
deleteFolder builddir []
|
||||||
maybe (pure ()) (\e => delete (outputdir </> e))
|
maybe (pure ()) (\e => delete (outputdir </> e))
|
||||||
(executable pkg)
|
(executable pkg)
|
||||||
|
-- clean out the generated docs
|
||||||
|
defs <- get Ctxt
|
||||||
|
let build = build_dir (dirs (options defs))
|
||||||
|
let docBase = build </> "docs"
|
||||||
|
let docDir = docBase </> "docs"
|
||||||
|
Right docfiles' <- coreLift $ listDir docDir
|
||||||
|
| Left err => pure ()
|
||||||
|
Right docfiles'' <- coreLift $ listDir docBase
|
||||||
|
| Left err => pure ()
|
||||||
|
traverse_ (\x => delete $ docDir </> x)
|
||||||
|
docfiles'
|
||||||
|
traverse_ (\x => delete $ docBase </> x)
|
||||||
|
docfiles''
|
||||||
|
deleteFolder docDir []
|
||||||
|
deleteFolder docBase []
|
||||||
runScript (postclean pkg)
|
runScript (postclean pkg)
|
||||||
where
|
where
|
||||||
delete : String -> Core ()
|
delete : String -> Core ()
|
||||||
|
Loading…
Reference in New Issue
Block a user