aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorThéo Zimmermann2018-10-22 09:19:13 +0200
committerThéo Zimmermann2018-10-22 09:19:13 +0200
commite605b73c34b0d796ac69e1953d3f5cb6975dfc0d (patch)
treec1278fa20cb0254147b65b9a9bfb01759dfbc647 /kernel
parentfd214f1ad31d88c76dd928b6c6b039eaefcb21db (diff)
parent32c1fc1ec2973a5b579f3e1f1ce6acf66488f24b (diff)
Merge PR #8784: [dune] Remove rule for cLexer.ml4 -> cLexer.ml
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions