Fix CI script filenames

This is a follow-up to GPR#1796
master
Sébastien Hinderer 2018-05-24 09:40:10 +02:00
parent 8ab50ec1e3
commit e3f792a14b
2 changed files with 0 additions and 0 deletions