From b123129f4e1ca1802ed4dbdeaf2aa83b9a7eb728 Mon Sep 17 00:00:00 2001
From: Victor Zverovich <victor.zverovich@gmail.com>
Date: Sat, 7 Nov 2020 08:42:08 -0800
Subject: [PATCH] Dump the content of html dir

---
 support/build-docs.py | 1 +
 1 file changed, 1 insertion(+)

diff --git a/support/build-docs.py b/support/build-docs.py
index 8ad86e9d..ea7a4063 100755
--- a/support/build-docs.py
+++ b/support/build-docs.py
@@ -51,6 +51,7 @@ 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'])