Merge pull request #62 from NightRa/patch-2

Display correct header for docs
idris-hackers · Sep 12, 2015 · 66bbce9 · 66bbce9
2 parents abc4b8c + 7c881c4
commit 66bbce9
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/lib/idris-controller.coffee b/lib/idris-controller.coffee
@@ -81,7 +81,7 @@ class IdrisController
       [type, highlightingInfo] = msg
       @messages.show()
       @messages.clear()
-      @messages.setTitle 'Idris: Type of <tt>' + word + '</tt>', true
+      @messages.setTitle 'Idris: Docs for <tt>' + word + '</tt>', true
       informationView = new InformationView
       informationView.initialize
         obligation: type