Raspbian, et Raspberry Pi OS utilisent par défaut PCManFM comme gestionnaire de fichier. Cette solution minimaliste, généralement suffisante, souffre néanmoins de fonctionnalités incomplètes.
C’est, en particulier, le cas des marque-pages (« bookmarks » dans la version anglaise) qui peut être crée mais pas supprimés du menu de ce gestionnaire de fichier (« file manager »).
C’est particulièrement embêtant lorsque le dossier correspondant au marque-page n’existe plus.
La configuration des marque-pages se trouvent dans le fichier ~/.config/gtk-3.0/bookmarks
.
Depuis le terminal, vous pouvez simplement l’éditer à l’aide de la commande suivante :
mousepad ~/.config/gtk-3.0/bookmarks
Mousepad est un éditeur de texte rapide pour l’environnement de bureau Xfce. C’est l’éditeur de texte par défaut sous Raspberry Pi OS.
Je vous propose le script suivant pcmanfm-bookmarks-cleaner.sh pour supprimer les marque-pages qui ne correspondent pas à un dossier existant.
Vous pouvez l'installer automatiquement, à partir d'un terminal, en vous mettant dans le répertoire de votre choix et avec les commandes:
wget https://blog.cclaude.rocks/post/2021/05/01/pcmanfm-bookmarks-cleaner.sh && chmod +x pcmanfm-bookmarks-cleaner.sh
-
Explication du script
La base du script est quelque chose comme cela :
while read -r entry ; do if [[ "${entry}" == 'file://'* ]] ; then dir="$( cut -d' ' -f1 <<<"${entry:7}" )" if [ -d "${dir}" ] ; then echo "OK: ${dir}" else echo "ERROR: ${dir}" fi else echo "IGNORE: ${entry}" fi done <~/.config/gtk-3.0/bookmarks
- On lit le fichier de configuration ligne par ligne.
- Si c’est un fichier, on extrait le nom du fichier (du dossier) — ici c’est une version simplifiée.
- Et on teste si le répertoire existe.
Le script final prend en compte que le nom du fichier est encodé (URL) et qu’il faut pour le cas général faire une conversion. Que ne souhaite pas modifier le fichier, si est OK.
Références
- Documentation de PCManFM en anglais
ᦿ