diff options
Diffstat (limited to 'python')
| -rw-r--r-- | python/clidef.py | 2 | ||||
| -rw-r--r-- | python/clippy/__init__.py | 15 |
2 files changed, 13 insertions, 4 deletions
diff --git a/python/clidef.py b/python/clidef.py index 8e3c7595b..aa6cd18b8 100644 --- a/python/clidef.py +++ b/python/clidef.py @@ -257,4 +257,4 @@ if __name__ == '__main__': process_file(args.cfile, ofd, dumpfd, args.all_defun) if args.o is not None: - clippy.wrdiff(args.o, ofd) + clippy.wrdiff(args.o, ofd, [args.cfile, os.path.realpath(__file__)]) diff --git a/python/clippy/__init__.py b/python/clippy/__init__.py index 82aa9495d..41aeae6b4 100644 --- a/python/clippy/__init__.py +++ b/python/clippy/__init__.py @@ -16,6 +16,7 @@ # with this program; see the file COPYING; if not, write to the Free Software # Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA +import os, stat import _clippy from _clippy import parse, Graph, GraphNode @@ -47,7 +48,7 @@ def dump(graph): for i, depth in graph_iterate(graph): print('\t%s%s %r' % (' ' * (depth * 2), i.type, i.text)) -def wrdiff(filename, buf): +def wrdiff(filename, buf, reffiles = []): '''write buffer to file if contents changed''' expl = '' @@ -57,8 +58,16 @@ def wrdiff(filename, buf): try: old = open(filename, 'r').read() except: pass if old == buf: + for reffile in reffiles: + # ensure output timestamp is newer than inputs, for make + reftime = os.stat(reffile)[stat.ST_MTIME] + outtime = os.stat(filename)[stat.ST_MTIME] + if outtime <= reftime: + os.utime(filename, (reftime + 1, reftime + 1)) # sys.stderr.write('%s unchanged, not written\n' % (filename)) return - with open('.new.' + filename, 'w') as out: + + newname = '%s.new-%d' % (filename, os.getpid()) + with open(newname, 'w') as out: out.write(buf) - os.rename('.new.' + filename, filename) + os.rename(newname, filename) |