A simpler way to avoid one makeinfo bug