publish docs on GH pages

2018-08-27 17:44:55 +02:00
parent a79ea9bee7
commit 3e39a0b927
5 changed files with 35 additions and 3 deletions
--- a/ci/script.sh
+++ b/ci/script.sh
@@ -67,4 +67,6 @@ EOF
    rm -rf $td
 }

-main
+if [ $TARGET != x86_64-unknown-linux-gnu ]; then
+    main
+fi