Commit 22da866
committed
doc(Tactic/MinImports): tidy backticks (leanprover-community#31861)
Found and fixed with help from Codex.
This is the last remaining true positive finding of the detection script in leanprover-community#31463.1 parent 5495d7e commit 22da866
1 file changed
Lines changed: 1 addition & 1 deletion
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
113 | 113 | | |
114 | 114 | | |
115 | 115 | | |
116 | | - | |
| 116 | + | |
117 | 117 | | |
118 | 118 | | |
119 | 119 | | |
| |||
0 commit comments