Reimplement refreshTerms to register names in the naming environment.#1284
Merged
brianhuffman merged 1 commit intomasterfrom issue869May 4, 2021
+4-4
Commits
Commits on May 3, 2021
- committed
Brian Huffman