(ciaopp) update use of @includefact

jfmc · jfmc · commit 7a8187cff148 · 2024-03-05T19:17:55.000+01:00
Src-commit: ff1dec2c88433582d79ed453be94b9feff3e22da
diff --git a/cmds/ciaopp-dump.pl b/cmds/ciaopp-dump.pl
@@ -21,9 +21,7 @@
 
    @section{Usage}
 
-   @begin{verbatim}
 @includefact{usage_text/1}
-   @end{verbatim}
 ").
 
 usage_text("ciaopp-dump <action> [<opts>] <files>
diff --git a/cmds/ciaoppcl.pl b/cmds/ciaoppcl.pl
@@ -15,9 +15,7 @@
 This interface can be used by means of the following command-line
 options:
 
-@begin{verbatim}
 @includefact{usage_message/1}
-@end{verbatim}
 
 @section{Description of the execution examples}
 
