binder folder needs to be in the root of the repo

lesteve · lesteve · commit b089c93ae13e · 2018-06-08T11:28:12.000+02:00
[doc build]
diff --git a/build_tools/circle/push_doc.sh b/build_tools/circle/push_doc.sh
@@ -47,7 +47,14 @@ cp -R $GENERATED_DOC_DIR $dir
 git config user.email "olivier.grisel+sklearn-ci@gmail.com"
 git config user.name $USERNAME
 git config push.default matching
-git add -f $dir/
+
+# binder folder for requirements needs to be at the root of the repo
+if [ -d dev/binder ]; then
+    rm -f binder
+    ln -s dev/binder
+    git add binder
+fi
+
 git commit -m "$MSG" $dir
 git push
-echo $MSG 
+echo $MSG
