From b2fcf8880ab687b5121f6bc1c457d5bcf69a142f Mon Sep 17 00:00:00 2001
From: Mike Gerwitz <mike@mikegerwitz.com>
Date: Sat, 19 Nov 2011 22:32:45 -0500
Subject: [PATCH] [#5] Corrected <= in doc Makefile for HTML replacement

---
 doc/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/Makefile b/doc/Makefile
index 88fed90..56d5179 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -23,7 +23,7 @@ doc_replace := s/<\/body>/<script type="text\/javascript" \
 	src="highlight.pack.js"><\/script><script type="text\/javascript" \
 	src="interactive.js"><\/script><\/body>/\
 	;s/\&gt\;=/\&\#8805\;/g\
-	;s/\&gt\;=/\&\#8804\;/g\
+	;s/\&lt\;=/\&\#8804\;/g\
 
 .PHONY: doc mkbuild-doc doc-img doc-pdf doc-info doc-plain doc-html