aboutsummaryrefslogtreecommitdiff
path: root/Makefile.ci
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-04-27 21:53:57 +0200
committerPierre-Marie Pédrot2020-04-27 21:53:57 +0200
commitd15b99d93b67f37a0c572950868713b2a7a2b1a4 (patch)
treee332379083cd993e343ac0995ab207963315a401 /Makefile.ci
parent2781da7585c56b836093940d7337cf18c4146faf (diff)
parent087804f288e82a5e4538b7b2387bdc324bebe7b6 (diff)
Merge PR #12073: Split off Nsatz tactic part into Nsatz_tactic
Reviewed-by: anton-trunov Reviewed-by: ppedrot
Diffstat (limited to 'Makefile.ci')
0 files changed, 0 insertions, 0 deletions