Pass the ci.skip option when pushing to git

Description

Pass the ci.skip option when pushing to git

This should prevent unwanted triggers of the CI.

Details

Committed
ltoscanoJun 17 2020, 11:23 PM
Parents
R883:1572199: Rewrite the handling of the local kdoctools sources
Branches
Unknown
Tags
Unknown