[galaxy-commits] galaxy-dist commit 7114d0f8d487: Fix for a bug I introduced in NoseHTML changes.