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

[ cleanup ] A few more cleanups

Browse Source
This commit is contained in:
Kamil Shakirov 2021-10-25 13:52:26 +06:00
parent 15d5c78447
commit 47326767ac
1 changed files with 10 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
src/Core/Options.idr
View File

@ -41,16 +41,16 @@ outputDirWithDefault d = fromMaybe (build_dir d </> "exec") (output_dir d)
public export
toString : Dirs -> String
toString d@(MkDirs wdir sdir bdir ldir odir dfix edirs pdirs ldirs ddirs) = """
Working Directory: \{ wdir }
Source Directory: \{ show sdir }
Build Directory: \{ bdir }
Local Depend Directory: \{ ldir }
Output Directory: \{ (outputDirWithDefault d) }
Installation Prefix: \{ dfix }
Extra Directories: \{ show edirs }
Package Directories: \{ show pdirs }
CG Library Directories: \{ show ldirs }
Data Directories: \{ show ddirs }
+ Working Directory :: \{ wdir }
+ Source Directory :: \{ show sdir }
+ Build Directory :: \{ bdir }
+ Local Depend Directory :: \{ ldir }
+ Output Directory :: \{ outputDirWithDefault d }
+ Installation Prefix :: \{ dfix }
+ Extra Directories :: \{ show edirs }
+ Package Directories :: \{ show pdirs }
+ CG Library Directories :: \{ show ldirs }
+ Data Directories :: \{ show ddirs }
"""
public export