From 1590d59eb73b2f2ba52a358fc83bee9bda0aea81 Mon Sep 17 00:00:00 2001
From: Mike Gerwitz <mike@mikegerwitz.com>
Date: Tue, 15 Nov 2011 23:24:19 -0500
Subject: [PATCH] [#5] Added gte and lte replacement for manual HTML output

---
 doc/Makefile | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/doc/Makefile b/doc/Makefile
index 87e3425..88fed90 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -21,7 +21,9 @@ doc_imgs_txt := $(patsubst %.dia, %.png, $(wildcard $(path_doc_img)/*.txt))
 
 doc_replace := s/<\/body>/<script type="text\/javascript" \
 	src="highlight.pack.js"><\/script><script type="text\/javascript" \
-	src="interactive.js"><\/script><\/body>/
+	src="interactive.js"><\/script><\/body>/\
+	;s/\&gt\;=/\&\#8805\;/g\
+	;s/\&gt\;=/\&\#8804\;/g\
 
 .PHONY: doc mkbuild-doc doc-img doc-pdf doc-info doc-plain doc-html