CI: use configflags instead of CONFIGFLAGS#1176

james-d-mitchell merged 1 commit into

semigroups:mainsemigroups/Semigroups:mainfrom

fingolfin:mh/configflagsfingolfin/Semigroups:mh/configflagsCopy head branch name to clipboard