diff options
| author | Pieter Wuille <pieter.wuille@gmail.com> | 2017-05-30 15:00:08 -0700 |
|---|---|---|
| committer | Pieter Wuille <pieter.wuille@gmail.com> | 2017-05-30 15:00:08 -0700 |
| commit | 5432fc3d59ce013d6c27f440ad86fc1f16d6e384 (patch) | |
| tree | 46801dcd8a813d6b112ce0516842f90450fc53b4 /contrib/devtools/github-merge.py | |
| parent | acd9957b72a21def0445d8a414ac39d88efe5d78 (diff) | |
Fail on commit with VERIFY SCRIPT but no scripted-diff
Diffstat (limited to 'contrib/devtools/github-merge.py')
0 files changed, 0 insertions, 0 deletions