diff options
author | Son Ho | 2022-02-09 11:43:56 +0100 |
---|---|---|
committer | Son Ho | 2022-02-09 11:43:56 +0100 |
commit | 2ec238154350c6ed8b2129828292b81752d4d750 (patch) | |
tree | 90622cbf59819d9a413c8d6917e79db9359e98aa /dune-project | |
parent | 56b17df2da3fa60d6c20de7288cc870767576827 (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 'dune-project')
0 files changed, 0 insertions, 0 deletions