Doc. system: fix semicolons

They were sometimes missing at the end of one-line headers.

diff --git a/build/doc-extract b/build/doc-extract
index 70de78e66dcc41e69741e0bd83f58f23f317b059..9ce8a3c5e06547e7cf6ae35e8404cabc16b25b9c 100755 (executable)
--- a/build/doc-extract
+++ b/build/doc-extract
@@ -52,6 +52,7 @@ sub formatNote( $$ ) {
        chomp $head;
         my( $type, $semicolon, $name, $oneline ) = detect( $head );
        $oneline =~ s/\s+$//;
+       $oneline =~ s/;?$/;/ if( $semicolon );
         $head =~ s/;?\s*$/;/ if( $semicolon );
        $head =~ s/(\.\.\.)/\\$1/g;
        print OUT "[[${type}_$name]]\n";