$$$

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).