90b21bcfb2
The echo commands following initialization of the "oldrun" variable need to be "tee"d to $oldrun/remote-log. This commit fixes several stragglers. Signed-off-by: Paul E. McKenney <paulmck@kernel.org> |
||
---|---|---|
.. | ||
bin | ||
configs | ||
doc | ||
formal/srcu-cbmc | ||
.gitignore | ||
Makefile |