jukoepke / hol-light

Automatically exported from code.google.com/p/hol-light
Other
0 stars 0 forks source link

code examples in documentation contain extra space #15

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago
Several code examples in documentation contain extra space after "#" char. 
Patch attached.

Original issue reported on code.google.com by piotr.tr...@gmail.com on 23 Jul 2014 at 8:49

Attachments:

GoogleCodeExporter commented 9 years ago
Thanks for the patch, finally applied in r205.

Original comment by jrh...@gmail.com on 16 Nov 2014 at 8:31