diff options
Diffstat (limited to 'src/run.bash')
| -rwxr-xr-x | src/run.bash | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/run.bash b/src/run.bash index 4bba1bf53b..64795b5e72 100755 --- a/src/run.bash +++ b/src/run.bash @@ -34,6 +34,12 @@ maketest \ (xcd lib; make test) || exit $? +(xcd lib/sync; +make clean; +time make +GOMAXPROCS=10 make test +) || exit $? + (xcd ../usr/gri/pretty make clean time make |