[MLton-commit] r5930

[Matthew Fluet]

Don't include MLTONWIKIVERSION file in pdf
----------------------------------------------------------------------

U   mlton/trunk/bin/make-pdf-guide

----------------------------------------------------------------------

Modified: mlton/trunk/bin/make-pdf-guide
===================================================================
--- mlton/trunk/bin/make-pdf-guide	2007-08-22 17:30:39 UTC (rev 5929)
+++ mlton/trunk/bin/make-pdf-guide	2007-08-22 19:07:58 UTC (rev 5930)
@@ -40,7 +40,7 @@
 
 # The grep -v takes out files that aren't wiki pages.
 # Hope that no files contain spaces or other specials -> `cat "$pages"` dies
-ls -1 | grep -v '\.' >"$pages"
+ls -1 | grep -v '\.' | grep -v "MLTONWIKIVERSION" >"$pages"
 
 echo 'Massaging HTML.'