diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-11-29 13:19:54 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-11-29 13:19:54 +0100 |
commit | b23df225c7df7883af6ecfa921986cfb6fd3cd7c (patch) | |
tree | 8d75179dec4c283260989363c372c4195f1aaa29 /tools/coqdep_common.ml | |
parent | 28dabf726be49bd47538642d1bae83990def4236 (diff) | |
parent | 19c4f594482d236d847990efbf00ebd2a80666ed (diff) |
Merge PR #6271: Add PR backport script.
Diffstat (limited to 'tools/coqdep_common.ml')
0 files changed, 0 insertions, 0 deletions