No-one puts info pages there. If /share does exist, it's likely to
contain remote file systems where access could be slow.
; Ref eg https://bugs.debian.org/786707
configure-info-directory)))
(prefixes
;; Directory trees in which to look for info subdirectories
- (prune-directory-list '("/usr/local/" "/usr/" "/opt/" "/")))
+ (prune-directory-list '("/usr/local/" "/usr/" "/opt/")))
(suffixes
;; Subdirectories in each directory tree that may contain info
;; directories.