helpers.inc.php

@@ -275,30 +275,6 @@ 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);