diff --git a/helpers.inc.php b/helpers.inc.php index 97380e7..0ba8f6d 100644 --- a/helpers.inc.php +++ b/helpers.inc.php @@ -275,6 +275,30 @@ function gen_file(string $tpl_file, string $result_file, $deps = array(), $force } } +function gen_to_dir(string $output_dir, array $rel_file2output) +{ + $existing_files = scan_files_rec([$output_dir]); + + $gen_files = []; + foreach($rel_file2output as $output_file => $output_text) + { + $gen_file = $output_dir.'/'.$output_file; + $gen_files[] = $gen_file; + ensure_write($gen_file, $output_text); + } + + $obsolete_files = array_diff( + array_map(function($file) { return normalize_path($file, true); }, $existing_files), + array_map(function($file) { return normalize_path($file, true); }, $gen_files) + ); + + foreach($obsolete_files as $file) + ensure_rm($file); + + //this is really important to change directory last modified time + touch($output_dir); +} + function ensure_read($file) { $c = file_get_contents($file);