diff options
| author | Emilio Jesus Gallego Arias | 2020-03-30 14:37:38 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-30 14:37:38 -0400 |
| commit | 5d912bfd5bb7dbd3634be9a204bb1fabf10223fe (patch) | |
| tree | 0bd787aee69ff63a57df5f8a63762d5790e382e4 /doc/plugin_tutorial/tuto3/_CoqProject | |
| parent | d2f21a119fea99d8621fb227b82fa8a1bf17d9fb (diff) | |
| parent | 2e3621d91f0306dbc9f0b576cd2f839e66390c42 (diff) | |
Merge PR #11968: Fix commit hook when there are no changes (eg amend message)
Reviewed-by: ejgallego
Diffstat (limited to 'doc/plugin_tutorial/tuto3/_CoqProject')
0 files changed, 0 insertions, 0 deletions