render \<circ> as o not &circ; (which is ^)
authorkleing
Mon, 29 Nov 2004 06:09:45 +0100
changeset 15336 cb35ae957c65
parent 15335 f81e6e24351f
child 15337 628d87767434
render \<circ> as o not &circ; (which is ^)
src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Thu Nov 25 20:33:35 2004 +0100
+++ b/src/Pure/Thy/html.ML	Mon Nov 29 06:09:45 2004 +0100
@@ -92,7 +92,7 @@
      | "\\<questiondown>" => (1.0, "&iquest;")
      | "\\<times>" => (1.0, "&times;")
      | "\\<div>" => (1.0, "&divide;")
-     | "\\<circ>" => (1.0, "&circ;")
+     | "\\<circ>" => (1.0, "o")
      | "\\<Alpha>" => (1.0, "&Alpha;")
      | "\\<Beta>" => (1.0, "&Beta;")
      | "\\<Gamma>" => (1.0, "&Gamma;")