Merge branch 'bugfix/master_out_of_sync' into 'master'

Merge github master branch



We have set up auto-push from release branch, but the CI script had `git push github HEAD:master` command in it.

Normally remote would reject the push from release branch into master because remote would have commits which the release branch didn't have.

But unit tests have been failing in master, so master branch wasn't deployed to Github recently, and Github master branch was behind the release branch. So the push from release branch into Github master went okay and now Gitlab master is behind Github master.



This PR merges Github master (which is now equal to release/v2.0) into Gitlab master so that automatic push can work again.



The original issue with push to master is also fixed.



See merge request !556

.gitlab-ci.yml

@@ -232,7 +232,7 @@ push_master_to_github:
     - chmod 600 ~/.ssh/id_rsa
     - echo -e "Host github.com\n\tStrictHostKeyChecking no\n" >> ~/.ssh/config
     - git remote add github git@github.com:espressif/esp-idf.git
-    - git push --follow-tags github HEAD:master
+    - git push --follow-tags github HEAD
 
 
 deploy_docs:
@@ -270,7 +270,7 @@ check_doc_links:
     - triggers
   script:
     # must be triggered with CHECK_LINKS=Yes, otherwise exit without test
-    - test $CHECK_LINKS = "Yes" || exit 0
+    - test "$CHECK_LINKS" = "Yes" || exit 0
     # can only run on master branch (otherwise the commit is not on Github yet)
     - test "${CI_BUILD_REF_NAME}" = "master" || exit 0
     - cd docs