gitlab-ci: Add a devel2 build

Authored by bgamari on Dec 21 2018, 11:59 PM.

Description

gitlab-ci: Add a devel2 build

Details

Committed
Marge Bot <ben+marge-bot@smart-cactus.org>Feb 7 2019, 12:55 AM
Parents
rGHCc07e7ecbdfc0: Fix #16287 by checking for more unsaturated synonym arguments
Branches
Unknown
Tags
Unknown
Marge Bot <ben+marge-bot@smart-cactus.org> committed rGHCc32de5f4f85b: gitlab-ci: Add a devel2 build (authored by bgamari).Feb 7 2019, 12:55 AM