summary refs log tree commit diff
path: root/src/doc/rustc-dev-guide
diff options
context:
space:
mode:
Diffstat (limited to 'src/doc/rustc-dev-guide')
-rwxr-xr-xsrc/doc/rustc-dev-guide/ci/check-in.sh13
1 files changed, 9 insertions, 4 deletions
diff --git a/src/doc/rustc-dev-guide/ci/check-in.sh b/src/doc/rustc-dev-guide/ci/check-in.sh
index d41a7ae5780..694c3bdf822 100755
--- a/src/doc/rustc-dev-guide/ci/check-in.sh
+++ b/src/doc/rustc-dev-guide/ci/check-in.sh
@@ -24,11 +24,16 @@ show_pulls() {
   jq -r '.[] | { title, number, html_url, user: .user.login } | "- " + .title + " [#" + (.number | tostring) + "](" + .html_url + ")"'
 }
 
-echo "Authors:"
-jq -r '{ login: .[].user.login } | "- **@" + .login + "**"' < pulls.json | sort -u
-echo "Changes:"
+echo "### Authors"
+jq -r '{ login: .[].user.login } | "- **@" + .login + "**"' < pulls.json \
+  | sort -u
+echo
+echo "### Changes"
+echo
 show_pulls < pulls.json
-echo "Changes in progress:"
+echo
+echo "### Changes in progress"
+echo
 # If there are more than 30 PRs open at a time, you'll need to set `per_page`.
 # For now this seems unlikely.
 curl "https://api.github.com/repos/rust-lang/rustc-dev-guide/pulls?state=open" | show_pulls