[O] The org paper manual - tools used

[Marcelo de Moraes Serpa]

Hey list,

The paper org manual was an exciting idea. I might buy one soon. I was
wondering how was the editing work involved in turning it into
paper-published book? What tools did you guys use?

Cheers,

- Marcelo.