summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorDavid Peter <sharkdp@users.noreply.github.com>2021-05-12 22:35:01 +0200
committerGitHub <noreply@github.com>2021-05-12 22:35:01 +0200
commitfb0f12a22175b15745aa24fbdd07c73609cadb46 (patch)
tree08086790bc8d57fdf89dcec7cc99d46f9e2722b7
parent9866408b7234503b1f1624522e0c94dd8ca32fb4 (diff)
parent09711cd6f9d1d163bddd068cb29b0a0ef49ff8c7 (diff)
Merge pull request #1643 from sharkdp/dependabot/submodules/assets/syntaxes/02_Extra/Lean-29a03a8
Bump assets/syntaxes/02_Extra/Lean from `824213d` to `29a03a8`
m---------assets/syntaxes/02_Extra/Lean0
1 files changed, 0 insertions, 0 deletions
diff --git a/assets/syntaxes/02_Extra/Lean b/assets/syntaxes/02_Extra/Lean
-Subproject 824213de37245140d75cdcffb3fbd6f61f73a97
+Subproject 29a03a8abaa884bde65b3c3dd1e46e87bb0fbfc