handle not configured with trailing flags

diff --git a/doc/misc/format-options.pl b/doc/misc/format-options.pl
index fa1727b22f69605261f70194fd6be5063267420b..af21225bf3672d8238eadefba7f0f017d2eebbe8 100644 (file)
--- a/doc/misc/format-options.pl
+++ b/doc/misc/format-options.pl
@@ -30,6 +30,7 @@ while (<>) {
        m!^( *)!;
        my $indent = $1;
        my $comment = "";
+       $line =~ s! // not configured,! //! if $strip_not_configured;
        $line =~ s! // not configured!! if $strip_not_configured;
        if ( $line =~ m!//.*! ) {
                $comment = $&;