bit
/
taskman_helpers
25
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Dir need regen support
Publish PHP Package / docker (push) Successful in 7s Details

This commit is contained in:
wrenge 2024-12-16 18:02:32 +03:00
parent 5b1a5ec442
commit 2e666d8b66
1 changed files with 9 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
helpers.inc.php
View File

@ -170,14 +170,21 @@ function json_make_pretty(string $json) : string
function need_to_regen(string $file, array $deps, bool $debug = false) : bool function need_to_regen(string $file, array $deps, bool $debug = false) : bool
{ {
if(!is_file($file)) if(is_file($file))
{
$fmtime = filemtime($file);
}
else if(is_dir($file))
{
$fmtime = filectime($file);
}
else
{ {
if($debug) if($debug)
echo "! $file\n"; echo "! $file\n";
return true; return true;
} }
$fmtime = filemtime($file);
foreach($deps as $dep) foreach($deps as $dep)
{ {
if($dep && is_file($dep) && (filemtime($dep) > $fmtime)) if($dep && is_file($dep) && (filemtime($dep) > $fmtime))