users guide: fix typesetting of pragmas
authorBen Price <ben@brprice.uk>
Tue, 22 Jan 2019 00:16:14 +0000 (00:16 +0000)
committerBen Gamari <ben@well-typed.com>
Wed, 23 Jan 2019 19:07:28 +0000 (14:07 -0500)
docs/users_guide/conf.py

index c64e0a3..e48992d 100644 (file)
@@ -147,9 +147,10 @@ def parse_ghci_cmd(env, sig, signode):
     return name
 
 def parse_pragma(env, sig, signode):
-    name = sig.split(' ')[0]
-    signode += addnodes.desc_name('{-# '+name, sig + ' #-}')
-    return name
+    idx = sig.split(' ')[0]
+    name = '{-# ' + sig + ' #-}'
+    signode += addnodes.desc_name(name, name)
+    return idx
 
 def parse_flag(env, sig, signode):