Remove debug code and fix bot contact

This commit is contained in:
Victor Zverovich 2020-11-07 09:16:55 -08:00
parent cd95579834
commit 2eb0be0b73
2 changed files with 2 additions and 5 deletions

View File

@ -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

View File

@ -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):