diff options
| author | Gaëtan Gilbert | 2020-10-09 21:56:24 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-10-26 14:42:15 +0100 |
| commit | 30f97beb1bfc149d9608cb74f24f69f268671e04 (patch) | |
| tree | 7423e52ead0509a4496fc40741664867d26db2ed /dev/tools/pre-commit | |
| parent | 5146b2f01b3b901ac99823d3a448c77560f248db (diff) | |
Ltac2: use ComTactic infrastructure
Diffstat (limited to 'dev/tools/pre-commit')
0 files changed, 0 insertions, 0 deletions