tools/linelength.py@2637134bc37c
tools/linelength.py
Fri, 01 Jul 2022 16:46:43 +0300
- author
- Teemu Piippo <teemu.s.piippo@gmail.com>
- date
- Fri, 01 Jul 2022 16:46:43 +0300
- changeset 312
- 2637134bc37c
- parent 114
- 4e03b0e2a29f
- permissions
- -rwxr-xr-x
Fix right click to delete not really working properly
Instead of removing the point that had been added, it would remove
the point that is being drawn, which would cause it to overwrite the
previous point using the new point, causing a bit of a delay
#!/usr/bin/env python3 import sys def check(filename): with open(filename) as file: for linenumber, line in enumerate(file, 1): if line[-1] == '\n': line = line[:-1] line = str.replace(line, '\t', ' ' * 4) if len(line) > 120: print(str.format( '{filename}:{linenumber}: warning: line length exceeds 120 characters', filename = filename, linenumber = linenumber ), file = sys.stderr) def main(): for filename in sys.argv[1:]: check(filename) return 0 if __name__ == '__main__': sys.exit(main())
