diff options
author | Peter Eisentraut | 2018-02-24 19:44:32 +0000 |
---|---|---|
committer | Peter Eisentraut | 2018-02-24 19:54:17 +0000 |
commit | c4ba1bee68abe217e441fb81343e5f9e9e2a5353 (patch) | |
tree | 4245980b7d67fae204a5ce54b9757a3337218a14 /src/tutorial/basics.source | |
parent | 9ee0573ef146ab37d7b85951f83e00bcbd305ff3 (diff) |
Update headers of generated files
The scripts were changed in c98c35cd084a25c6cf9b08c76de8b89facd75fe7,
but the output files were not updated to reflect the script changes.
Diffstat (limited to 'src/tutorial/basics.source')
0 files changed, 0 insertions, 0 deletions