summaryrefslogtreecommitdiff
path: root/src/jib/jib_interactive.ml
diff options
context:
space:
mode:
authorAlasdair Armstrong2020-01-10 18:58:55 +0000
committerAlasdair Armstrong2020-01-10 19:48:45 +0000
commit1257411d702a12cde9d1aef5cdd85e18307812d9 (patch)
treef19b3ebf8fe4088435897cd8b6d4c2cdcd38f016 /src/jib/jib_interactive.ml
parent8809d3154fcd6950c8cc2abc1a946eb6924f7836 (diff)
Don't do any C specific name mangling for the cons operator in jib_compile
Instead handle it specially in c_backend, leaving the type information in the IR available for other consumers
Diffstat (limited to 'src/jib/jib_interactive.ml')
0 files changed, 0 insertions, 0 deletions