diff options
Diffstat (limited to 'docs/users_guide/conf.py')
| -rw-r--r-- | docs/users_guide/conf.py | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/docs/users_guide/conf.py b/docs/users_guide/conf.py index 6fd94db74f..d69c84f914 100644 --- a/docs/users_guide/conf.py +++ b/docs/users_guide/conf.py @@ -284,7 +284,17 @@ def setup(app): parse_node=parse_flag, indextemplate='pair: %s; RTS option', doc_field_types=[ + Field('since', label='Introduced in GHC version', names=['since']) + ]) + + app.add_object_type('event-type', 'event-type', + objname='event log event type', + indextemplate='pair: %s; eventlog event type', + doc_field_types=[ Field('since', label='Introduced in GHC version', names=['since']), + Field('tag', label='Event type ID', names=['tag']), + Field('length', label='Record length', names=['length']), + TypedField('fields', label='Fields', names='field', typenames=('fieldtype', 'type')) ]) app.add_object_type('pragma', 'pragma', |