diff options
| author | Jason Gross | 2020-01-09 13:55:00 -0500 |
|---|---|---|
| committer | Jason Gross | 2020-01-09 13:55:00 -0500 |
| commit | b9f1d79e188242508dcf29803484b93a4d8e836f (patch) | |
| tree | e53a90f688b1b3bd26218dd32bf83e2232423972 /plugins/syntax/string_notation.mli | |
| parent | a9a06ffbd8aa4b5491227b6ef0e63831101b913f (diff) | |
| parent | d8d5631ed89b645e2bce50203a877ef5b5ab4fab (diff) | |
Merge PR #11371: [merge script] Never bypass outdated branch sanity check.
Reviewed-by: JasonGross
Diffstat (limited to 'plugins/syntax/string_notation.mli')
0 files changed, 0 insertions, 0 deletions