diff options
author | Jim Meyering <meyering@fb.com> | 2018-02-03 16:57:36 -0800 |
---|---|---|
committer | Jim Meyering <meyering@fb.com> | 2018-02-03 16:57:36 -0800 |
commit | 67f682f1d3b5a61e7d55db63323f1233347f8e18 (patch) | |
tree | b2d3b99fc71530f3e74763c00678f414cb7f5d8d /top/maint.mk | |
parent | ab4b1f3d4e517a0948fce56d6c0ac0995fd5133b (diff) | |
download | gnulib-67f682f1d3b5a61e7d55db63323f1233347f8e18.tar.gz |
maint.mk: exempt "/proc/filesystems" from "file system" syntax check
* top/maint.mk (sc_file_system): Don't complain about
"/proc/filesystems".
Diffstat (limited to 'top/maint.mk')
-rw-r--r-- | top/maint.mk | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/top/maint.mk b/top/maint.mk index be86fb5d52..508c2f7c39 100644 --- a/top/maint.mk +++ b/top/maint.mk @@ -421,6 +421,7 @@ sc_error_message_period: sc_file_system: @prohibit=file''system \ + exclude='/proc/filesystems' \ ignore_case=1 \ halt='found use of "file''system"; spell it "file system"' \ $(_sc_search_regexp) |