From b0cd2d8e5255cdddea989f61f93d0cb4c0eec304 Mon Sep 17 00:00:00 2001
From: pdiogoantunes <pdiogoantunes+gitit@evolix.fr>
Date: Wed, 19 Jul 2017 12:55:37 +0200
Subject: [PATCH] ajout proc

---
 TipsShell.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/TipsShell.md b/TipsShell.md
index 651ce75e..249ce165 100644
--- a/TipsShell.md
+++ b/TipsShell.md
@@ -206,7 +206,7 @@ echo /etc/$file :; diff /etc/$file <(ssh REMOTE cat /etc/$file); done
 Quand il s'agit de / - penser à exclure les autres partitions (si existante de toute évidence) :
 
 ~~~
-# ncdu / --exclude /home --exclude /srv --exclude /var --exclude /tmp --exclude /boot --exclude /usr
+# ncdu / --exclude /home --exclude /srv --exclude /var --exclude /tmp --exclude /boot --exclude /usr --exclude /proc
 ~~~
 
 Pour certaines anciennes versions :