From c560dd07f506810eaabae2f582491138aa224819 Mon Sep 17 00:00:00 2001 From: Ben Gamari Date: Thu, 23 Apr 2020 22:57:24 -0400 Subject: users guide: Move eventlog documentation users guide --- docs/users_guide/conf.py | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'docs/users_guide/conf.py') 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 @@ -283,8 +283,18 @@ def setup(app): objname='runtime system command-line option', 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', -- cgit v1.2.1