diff --git a/doc/build.py b/doc/build.py index cdcea691..00396bfa 100755 --- a/doc/build.py +++ b/doc/build.py @@ -103,8 +103,6 @@ def build_docs(version='dev', **kwargs): os.path.join(html_dir, '_static', 'fmt.css')] print("Running {}".format(cmd)) check_call(cmd) - sys.stdout.flush() - check_call(['ls', '-R', os.path.join(html_dir, '_static')]) except OSError as e: if e.errno != errno.ENOENT: raise diff --git a/support/build-docs.py b/support/build-docs.py index 7cb32894..2fddecd0 100755 --- a/support/build-docs.py +++ b/support/build-docs.py @@ -50,11 +50,10 @@ check_call(['git', 'clone', git_url + 'fmtlib/{}.git'.format(repo)]) # Copy docs to the repo. target_dir = os.path.join(repo, 'dev') rmtree_if_exists(target_dir) -check_call(['ls', '-R', html_dir]) shutil.copytree(html_dir, target_dir, ignore=shutil.ignore_patterns('.*')) if is_ci: - check_call(['git', 'config', '--global', 'user.name', 'amplbot']) - check_call(['git', 'config', '--global', 'user.email', 'viz@ampl.com']) + check_call(['git', 'config', '--global', 'user.name', 'fmtbot']) + check_call(['git', 'config', '--global', 'user.email', 'viz@fmt.dev']) # Push docs to GitHub pages. check_call(['git', 'add', '--all'], cwd=repo) if call(['git', 'diff-index', '--quiet', 'HEAD'], cwd=repo):