Dédoubler la taille du cache des fichiers produits - fixes #4921

Désencombrer le cache des fichiers produits en créant un fichier quasivide qui ne sert que pour son filemtime, au lieu de garder à cet usage une pleine copie du fichier produit, qui peut être gros et peut produire un dossier de cache gigantesque après quelques jours ou années

• fixes #4921 (closed)
• squash de #4925 + minifix

Lorsque #PRODUIRE ou produire_fond_statique produisent des gros fichiers, ce fix divise par 2 la taille mobilisée dans les sous dossiers de /local.