New workaround for temp dir on different device.

Currently, on setups where the project dir is on a different file system as the system temporary directory, a temporary directory is instead created on the project dir. This is not very nice.

With this change, we still create temporary files in the system temporary directory but copy instead of move files from and to the temporary directory, if necessary, which solves the problems.

1 files changed, 20 insertions, 1 deletions

diff --git a/support/lib/util.py b/support/lib/util.py
index f6d8f8a..3a852f4 100644
--- a/support/lib/util.py
+++ b/support/lib/util.py
@@ -5,6 +5,25 @@ class UserError(Exception):
 	pass
 
 
+def rename_atomic(source_path, target_path):
+	"""
+	Move the file at source_path to target_path.
+	
+	If both paths reside on the same device, os.rename() is used, otherwise the file is copied to a temporary name next to target_path and moved from there using os.rename().
+	"""
+	
+	source_dir_stat = os.stat(os.path.dirname(source_path))
+	target_dir_stat = os.stat(os.path.dirname(target_path))
+	
+	if source_dir_stat.st_dev == target_dir_stat.st_dev:
+		os.rename(source_path, target_path)
+	else:
+		temp_path = target_path + '~'
+		
+		shutil.copyfile(source_path, temp_path)
+		os.rename(temp_path, target_path)
+
+
 @contextlib.contextmanager
 def TemporaryDirectory():
 	dir = tempfile.mkdtemp()
@@ -32,7 +51,7 @@ def command(args, remove_env = [], set_env = { }):
 
 
 def bash_escape_string(string):
-	return "'{}'".format(re.sub("'", "'\"'\"'", string))	
+	return "'{}'".format(re.sub("'", "'\"'\"'", string))
 
 
 def write_file(path, data):