bug#15257: stat and df report different filesystems for /dev

[C de-Avillez]

original Ubuntu bug: https://bugs.launchpad.net/bugs/1219529

Tested on linux 3.11.RC7 and 3.8.8, coreutils 8.20 and 8.21

When trying to use 'df -x tmpfs', /dev is still shown:

address@hidden:~$ df -x tmpfs | grep udev
udev              247532       8    247524   1% /dev

But 'stat' reports the filesystem as 'tmpfs':

address@hidden:~$ stat -f /dev
  File: "/dev"
    ID: 0        Namelen: 255     Type: tmpfs
Block size: 4096       Fundamental block size: 4096
Blocks: Total: 61883      Free: 61881      Available: 61881
Inodes: Total: 61883      Free: 61479

This seems to happen because -- really -- the type is 'devtmpfs':

address@hidden:~$ mount | grep udev
udev on /dev type devtmpfs (rw,mode=0755)

And, indeed, running 'df -x devtmpfs' works:

address@hidden:~$ df -x devtmpfs
Filesystem     1K-blocks    Used Available Use% Mounted on
/dev/vda        20511356 2518320  16944460  13% /
none                   4       0         4   0% /sys/fs/cgroup
tmpfs              50300     232     50068   1% /run
none                5120       0      5120   0% /run/lock
none              251484      52    251432   1% /run/shm
none              102400       0    102400   0% /run/user

I feel this is incorrect: even though 'info mount' does not list devtmpfs
as a possible FS type (which might be another bug in itself, but outside
coreutils), at least 'stat' and 'df' should be consistent on their output.

Cheers,

-- 
..hggdh..