aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorJim Fehrle2020-10-11 18:39:16 -0700
committerJim Fehrle2020-10-27 12:15:35 -0700
commitb402adc12c00ba72046423d3a1737ccad517f70e (patch)
tree1940efc064bf87b9b996a0e21eaa75e9b57605d4 /dev
parent5f5cddae48c08872107f30938dcc2f3c8d91f33a (diff)
Rename operconstr -> term
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions