tree c4b8e58334f23a24b6d4905a8d5f7b55f1609b7d
parent aa108fcc979350f3f7245569a76196b11d033b91
author Jan Kundrát <jan.kundrat@cesnet.cz> 1639504283 +0100
committer Michal Vasko <mvasko@cesnet.cz> 1639653123 +0100

CI: remove an unused job

This was used for the coverity job before, but that one got moved to
another file.

Fixes: 7f55a30c actions REFACTOR separate devel push actions