# HG changeset patch
# User kleing
# Date 1101704985 -3600
# Node ID cb35ae957c6516b141e323e39fc3c4ad8d212ab2
# Parent  f81e6e24351f7f8c226f638daea132347788b84b
render \<circ> as o not &circ; (which is ^)

diff -r f81e6e24351f -r cb35ae957c65 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;")