diff options
| author | Scott Shawcroft <scott@tannewt.org> | 2018-07-30 12:33:44 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-07-30 12:33:44 -0700 |
| commit | a6d94b68453b8535398ff0b61cd6c4a0c7f77f8b (patch) | |
| tree | 8defd6392975b8145dc11f0cce9c39a4e440b32a /py/makeversionhdr.py | |
| parent | 433a29bb70d51abb84c77a911ced43c6ff14706e (diff) | |
| parent | b1006170f1dcfa3a9499ef31c19c8f20736b136a (diff) | |
Merge pull request #1068 from dhalbert/micropython-25ae98f-merge
Micropython 25ae98f merge
Diffstat (limited to 'py/makeversionhdr.py')
| -rw-r--r-- | py/makeversionhdr.py | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/py/makeversionhdr.py b/py/makeversionhdr.py index 1f82d5933..89a604aeb 100644 --- a/py/makeversionhdr.py +++ b/py/makeversionhdr.py @@ -100,7 +100,7 @@ def make_version_header(filename): # Only write the file if we need to if write_file: - print("Generating %s" % filename) + print("GEN %s" % filename) with open(filename, 'w') as f: f.write(file_data) |