extension→. [gestion de fichiers] [extension]. Extension de nom de fichier utilisée pour désigner certains fichiers temporaires (généralement sous MS-DOS, c'est donc devenu rare).
