diff options
Diffstat (limited to 'docs/users_guide')
| -rw-r--r-- | docs/users_guide/conf.py | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/docs/users_guide/conf.py b/docs/users_guide/conf.py index c64e0a3693..e48992d405 100644 --- a/docs/users_guide/conf.py +++ b/docs/users_guide/conf.py @@ -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): |