diff --git a/doc/misc/format-options.pl b/doc/misc/format-options.pl
index fa1727b22f..af21225bf3 100644
--- 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 = $&;