From 71e3a99742a67739f8b1b02087984935998f932d Mon Sep 17 00:00:00 2001 From: "mergify[bot]" <37929162+mergify[bot]@users.noreply.github.com> Date: Thu, 19 Nov 2020 21:41:23 +0000 Subject: [PATCH] fix doc redirects (#13709) (#13710) (cherry picked from commit af08ba93e66a033c563d9eb61b202cff29abda29) Co-authored-by: Jack May --- docs/publish-docs.sh | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/docs/publish-docs.sh b/docs/publish-docs.sh index 51da9c9b58..33bcbf0653 100755 --- a/docs/publish-docs.sh +++ b/docs/publish-docs.sh @@ -31,17 +31,17 @@ cat > "$CONFIG_FILE" <