diff options
author | makaimann <makaim@stanford.edu> | 2019-06-28 02:36:16 -0700 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2019-06-28 02:36:16 -0700 |
commit | 3777d6c940818a8085dbcc7a83f6d82adf4ced0f (patch) | |
tree | 0a13fab8ea58d0ae920f15371771090928a0976b /src/options | |
parent | 0a936446c8e2d95e5c7d39f2f3f0740fb5b717a5 (diff) |
Make mkOpTerm const (#3072)
Diffstat (limited to 'src/options')
0 files changed, 0 insertions, 0 deletions