[temp] Replace \term with \defn or \placeholder#1370
Merged
zygoloid merged 1 commit intocplusplus:masterfrom Feb 6, 2017
Merged
[temp] Replace \term with \defn or \placeholder#1370zygoloid merged 1 commit intocplusplus:masterfrom
zygoloid merged 1 commit intocplusplus:masterfrom
