From 22df7c66edc89c218fc1886160e69f353bbb3036 Mon Sep 17 00:00:00 2001 From: "Ryan C. Gordon" Date: Fri, 21 Nov 2025 09:36:56 -0500 Subject: [PATCH] wikiheaders: Treat docs/INTRO-* files the same way as the README files. Closes #14261. --- build-scripts/wikiheaders.pl | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/build-scripts/wikiheaders.pl b/build-scripts/wikiheaders.pl index 6e542c66f7..6e46547608 100755 --- a/build-scripts/wikiheaders.pl +++ b/build-scripts/wikiheaders.pl @@ -2149,7 +2149,7 @@ if ($copy_direction == 1) { # --copy-to-headers opendir(DH, $wikipath) or die("Can't opendir '$wikipath': $!\n"); while (readdir(DH)) { my $dent = $_; - if ($dent =~ /\AREADME\-.*?\.md\Z/) { # we only bridge Markdown files here that start with "README-". + if ($dent =~ /\A(README|INTRO)\-.*?\.md\Z/) { # we only bridge Markdown files here that start with "README-" or "INTRO-". filecopy("$wikipath/$dent", "$readmepath/$dent", "\n"); } } @@ -2762,7 +2762,7 @@ __EOF__ opendir(DH, $readmepath) or die("Can't opendir '$readmepath': $!\n"); while (my $d = readdir(DH)) { my $dent = $d; - if ($dent =~ /\AREADME\-.*?\.md\Z/) { # we only bridge Markdown files here that start with "README-". + if ($dent =~ /\A(README|INTRO)\-.*?\.md\Z/) { # we only bridge Markdown files here that start with "README-" or "INTRO". filecopy("$readmepath/$dent", "$wikipath/$dent", "\n"); } } @@ -2772,7 +2772,7 @@ __EOF__ opendir(DH, $wikipath) or die("Can't opendir '$wikipath': $!\n"); while (my $d = readdir(DH)) { my $dent = $d; - if ($dent =~ /\A(README\-.*?)\.md\Z/) { + if ($dent =~ /\A((README|INTRO)\-.*?)\.md\Z/) { push @pages, $1; } }