tools/fast: fix uploading

pull/11204/head
Alexander Medvednikov 2021-08-16 08:33:53 +03:00
parent 22b1fca793
commit e09d3eef5f
1 changed files with 2 additions and 1 deletions

View File

@ -118,7 +118,8 @@ fn main() {
// exec('git checkout master')
// os.write_file('last_commit.txt', commits[commits.len - 1]) ?
// Upload the result to github pages
if os.args.contains('upload') {
if os.args.contains('-upload') {
println('uploading...')
os.chdir('website')
os.execute_or_exit('git checkout gh-pages')
os.cp('../index.html', 'index.html') ?