From d18ee5afe8b1992d234402cd71f809cd904113a5 Mon Sep 17 00:00:00 2001
From: ebraminio <ebrahim@gnu.org>
Date: Thu, 2 Nov 2017 07:56:25 -0700
Subject: [PATCH] Copy dummy docs/circle.yml to gh-pages branch (#603)

---
 .ci/deploy-docs.sh | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.ci/deploy-docs.sh b/.ci/deploy-docs.sh
index e4dbad44d..d647cb4d5 100755
--- a/.ci/deploy-docs.sh
+++ b/.ci/deploy-docs.sh
@@ -16,6 +16,7 @@ mkdir $DOCSDIR
 cd $DOCSDIR
 
 cp ../docs/html/* .
+cp ../docs/circle.yml .
 
 git init
 git config user.name "Travis CI"