alaviss 40898871a9 workflows/ci_docs: fix documentation deployment (#13819) ... * workflows/ci_docs: fix docs publishing It turns out that github.ref is the full ref name, so we have to be a bit more specific. See https://developer.github.com/v3/activity/events/types/#pushevent Also fixed a silly typo :) * workflows/ci_docs: run CI when there are changes to the workflow		2020-03-31 19:36:37 +02:00
..
ci.yml.disabled	workflows/ci: disable	2020-03-17 08:48:42 +01:00
ci_docs.yml	workflows/ci_docs: fix documentation deployment (#13819)	2020-03-31 19:36:37 +02:00
ci_ssl.yml	SSL certificate verify GitHub action (#13697)	2020-03-20 17:11:39 +01:00