dejagnu: add description for "dejagnu" command

This commit is contained in:
Xi Ruoyao 2022-02-17 18:49:10 +08:00
parent 85d9756bbe
commit 24fe054b4e
No known key found for this signature in database
GPG Key ID: D95E4716CCBB34DC

View File

@ -74,7 +74,7 @@ install -v -m644 doc/dejagnu.{html,txt} /usr/share/doc/dejagnu-&dejagnu-versio
<segtitle>Installed program</segtitle>
<seglistitem>
<seg>runtest</seg>
<seg>dejagnu and runtest</seg>
</seglistitem>
</segmentedlist>
@ -83,6 +83,16 @@ install -v -m644 doc/dejagnu.{html,txt} /usr/share/doc/dejagnu-&dejagnu-versio
<?dbfo list-presentation="list"?>
<?dbhtml list-presentation="table"?>
<varlistentry id="dejagnu">
<term><command>dejagnu</command></term>
<listitem>
<para>DejaGNU auxiliary command launcher</para>
<indexterm zone="ch-system-dejagnu dejagnu">
<primary sortas="b-dejagnu">dejagnu</primary>
</indexterm>
</listitem>
</varlistentry>
<varlistentry id="runtest">
<term><command>runtest</command></term>
<listitem>