tools/fast: push changes to gh pages

pull/8615/head
Alexander Medvednikov 2021-02-07 03:35:22 +01:00
parent d77bb2f606
commit d284918554
1 changed files with 1 additions and 0 deletions

View File

@ -33,6 +33,7 @@ fn main() {
os.exec('git checkout gh-pages') ?
os.cp('../index.html', 'index.html') ?
os.system('git commit -am "update benchmark"')
os.system('git push origin gh-pages')
os.chdir('..')
}
println('sleeping 20')