Commit 02b17cd
Fail if a patch is not applicable, as suggested by Jason here: MetaRocq#791 (comment)
Co-authored-by: Jason Gross <jgross@mit.edu>1 parent 486d222 commit 02b17cd
1 file changed
+2
-2
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
19 | 19 | | |
20 | 20 | | |
21 | 21 | | |
22 | | - | |
23 | | - | |
| 22 | + | |
| 23 | + | |
24 | 24 | | |
25 | 25 | | |
26 | 26 | | |
| |||
0 commit comments