Comment 4 for bug 832123

As a point of reference, I did the same as above, but on a natty host:

root@ubuntu:/# cat /proc/1/mountinfo
68 75 0:24 / /dev/pts rw,relatime - devpts devpts rw,mode=600,ptmxmode=666
72 50 252:0 /home/ubuntu/root / rw,relatime - ext4 /dev/disk/by-label/uec-rootfs rw,barrier=1,data=ordered
73 72 0:24 / /dev/pts rw,relatime - devpts devpts rw,mode=600,ptmxmode=666
75 72 0:28 / /dev rw,relatime - tmpfs /dev rw
76 72 0:26 / /proc rw,relatime - proc /proc rw
77 72 0:29 / /sys rw,relatime - sysfs /sys rw

root@ubuntu:/# cat /proc/mounts
rootfs / rootfs rw 0 0
devpts /dev/pts devpts rw,relatime,mode=600,ptmxmode=666 0 0
/dev/disk/by-label/uec-rootfs / ext4 rw,relatime,barrier=1,data=ordered 0 0
devpts /dev/pts devpts rw,relatime,mode=600,ptmxmode=666 0 0
/dev /dev tmpfs rw,relatime 0 0
/proc /proc proc rw,relatime 0 0
/sys /sys sysfs rw,relatime 0 0

So, although it does seem strange to me that /dev is mounted *over* /dev/pts, it was that way in natty also.