diff options
| author | Richard W.M. Jones <rjones@redhat.com> | 2012-09-24 09:26:45 +0100 |
|---|---|---|
| committer | Richard W.M. Jones <rjones@redhat.com> | 2012-09-24 09:34:33 +0100 |
| commit | a3d7f5bc17aa3935a427812a49de60ecc0a345ca (patch) | |
| tree | 875356253735ff8f15bc8dd41cb0602aeb7b8b7c /python/examples | |
| parent | 1949016e899b2737525fdc9b6dda451ad9ecbd66 (diff) | |
generator: The default input files are 'generator/ *.ml' [sic].
Since generator source files were renamed, the comment at the
top of each generated file was wrong.
Unfortunately we cannot allow /* to appear within a comment,
so the space is necessary.
Diffstat (limited to 'python/examples')
0 files changed, 0 insertions, 0 deletions