Comment 7 for bug 933903

Thanks for the quick response. Just read that the debbug: http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=632656 has a different patch which has not been applied to debian. Not sure if we should be picking up this patch, in case debian goes with the other patch as to not be divergent, or if we should suggest debian pick up this patch. The difference between patches are the following:

--

This is the debian patch which also fixes a space issue with the /proc/filesystems grep. In addition it doesn't rely on mountpoint (although not sure this is a major issue):

+grep -Eq '[[:space:]]devpts$' /proc/filesystems 2>/dev/null || exit 0
+grep -Eq 'devpts[[:space:]]' /proc/mounts 2>/dev/null && exit 0

Here is my patch which was just applied:

+# If /dev/pts is already mounted, don't re-mount it.
+mountpoint -q /dev/pts || exit 0