add comment

RalfJung · RalfJung · commit 3a837cdedd78 · 2019-05-27T15:19:53.000+02:00
diff --git a/travis.sh b/travis.sh
@@ -17,6 +17,8 @@ echo
 # Test
 function run_tests {
     ./miri test
+    # "miri test" has built the sysroot for us, now this should pass without
+    # any interactive questions.
     test-cargo-miri/run-test.py
 }
 

Original file line number	Diff line number	Diff line change
`@@ -17,6 +17,8 @@ echo`
`17`	`17`	`# Test`
`18`	`18`	`function run_tests {`
`19`	`19`	`./miri test`
	`20`	`+ # "miri test" has built the sysroot for us, now this should pass without`
	`21`	`+ # any interactive questions.`
`20`	`22`	`test-cargo-miri/run-test.py`
`21`	`23`	`}`
`22`	`24`