remove outdated comment

RalfJung · RalfJung · commit 4951d5f40413 · 2023-07-03T11:59:19.000+02:00
diff --git a/src/tools/miri/.github/workflows/ci.yml b/src/tools/miri/.github/workflows/ci.yml
@@ -135,7 +135,6 @@ jobs:
   # workflow is successful listening to webhooks only.
   #
   # ALL THE PREVIOUS JOBS NEED TO BE ADDED TO THE `needs` SECTION OF THIS JOB!
-  # (`fmt` is deliberately not listed, we want bors to ignore it.)
   end-success:
     name: bors build finished
     runs-on: ubuntu-latest

Original file line number	Diff line number	Diff line change
`@@ -135,7 +135,6 @@ jobs:`
`135`	`135`	`# workflow is successful listening to webhooks only.`
`136`	`136`	`#`
`137`	`137`	# ALL THE PREVIOUS JOBS NEED TO BE ADDED TO THE `needs` SECTION OF THIS JOB!
`138`		- # (`fmt` is deliberately not listed, we want bors to ignore it.)
`139`	`138`	`end-success:`
`140`	`139`	`name: bors build finished`
`141`	`140`	`runs-on: ubuntu-latest`