Comment faire le ménage après l’installation d’une extension ?#

Il n’y a généralement pas grand-chose à faire une fois que vous avez terminé l’installation d’une extension.

Les choses que vous pouvez supprimer sont :

  • le fichier d’archive lui-même, si vous avez récupéré l’extension sous forme d’un fichier ZIP ou équivalent ;

  • les fichiers DTX et INS, si vous avez choisi de ne pas les installer avec la documentation ;

  • et les fichiers AUX, LOG, IDX, etc., générés par la compilation de la documentation.

Un moyen de se faciliter la vie est de télécharger l’archive dans un répertoire temporaire, puis de supprimer ce répertoire et son contenu une fois l’installation terminée.