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

mmhelloworld · Jul 16, 2021 · 7e904ec · 7e904ec
1 parent 9fc3ee7
commit 7e904ec
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr
@@ -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"