summaryrefslogtreecommitdiff
path: root/.gitignore
diff options
context:
space:
mode:
authorNadrieril2019-04-23 17:16:29 +0200
committerNadrieril2019-04-23 17:16:29 +0200
commita97ebd37169193c6392658aa8b022c7e0f8c4a34 (patch)
tree8764f6375d2164e061e0f1b7f04e27a6537b7ab1 /.gitignore
parent2f1fa26abd9c9f2b75d24b18877d3b278f7d2a01 (diff)
Avoid constructing ExprF::Pi while typechecking
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions