patch so DocumentPrinter.java can be removed