diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-08 18:28:55 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-10 09:54:41 +0200 |
commit | 63510329fae28f7a9d18935f24e3ebf0485dabc8 (patch) | |
tree | 2e9dccf5915300671afd61cd2070156dd2174f68 /tactics | |
parent | 7f17e151c0a2666263d3854c064acdfea29edf53 (diff) |
A more regular naming of variables in test-suite Makefile.
Diffstat (limited to 'tactics')
0 files changed, 0 insertions, 0 deletions