aboutsummaryrefslogtreecommitdiff
path: root/.gitignore
diff options
context:
space:
mode:
authorTristan Riehs <tristan.riehs@inria.fr>2026-05-03 13:51:18 +0200
committerTristan Riehs <tristan.riehs@inria.fr>2026-05-03 13:51:18 +0200
commit1809322f080a2a9eedeb32b9b6bf1bafa8ce8d15 (patch)
tree9639c85eea671f9b5a9726faabb63b66f611ca33 /.gitignore
parent0c41b30e1534e4e23a1ff15eca50247579071d83 (diff)
Add make check in the readme
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions