Fix for bug #688 (documentation building)