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

Update %hide help to show it takes a 'name'.

Browse Source
This commit is contained in:
Thomas E. Hansen 2021-07-16 09:58:33 +02:00
parent 9fc3ee79e1
commit 7e904ecdef
No known key found for this signature in database
GPG Key ID: 27727D7EC6CB4F4C
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Idris/Syntax.idr
View File

@ -293,7 +293,7 @@ mutual
show $ vsep $ map (((<++>) "+") . pretty {ann=()} . showDirective) $ filter isPragma directiveList
where
showDirective : Directive -> String
showDirective (Hide _) = "%hide term"
showDirective (Hide _) = "%hide name"
showDirective (Logging _) = "%logging [topic] lvl"
showDirective (LazyOn _) = "%auto_lazy on|off"
showDirective (UnboundImplicits _) = "%unbound_implicits"