summaryrefslogtreecommitdiff
path: root/src/Identifiers.ml
diff options
context:
space:
mode:
authorSon Ho2022-02-09 11:43:56 +0100
committerSon Ho2022-02-09 11:43:56 +0100
commit2ec238154350c6ed8b2129828292b81752d4d750 (patch)
tree90622cbf59819d9a413c8d6917e79db9359e98aa /src/Identifiers.ml
parent56b17df2da3fa60d6c20de7288cc870767576827 (diff)
Improve a bit the quality of the generated code by adjusting the
function suffixes depending on whether forward/backward translations have been filtered
Diffstat (limited to '')
0 files changed, 0 insertions, 0 deletions