From 7e904ecdefa6a0476ffb9e4899073cf0ab7d4d29 Mon Sep 17 00:00:00 2001
From: "Thomas E. Hansen" <teh6@st-andrews.ac.uk>
Date: Fri, 16 Jul 2021 09:58:33 +0200
Subject: [PATCH] Update `%hide` help to show it takes a 'name'.

---
 src/Idris/Syntax.idr | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr
index 879c45a50..3414a6394 100644
--- 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"