Explain that multiple file descriptors for a single file are

independent.
From Godmar Back.

diff --git a/doc/userprog.texi b/doc/userprog.texi
index 11d9875ce7beabe78e2ebb8e9079d7402bb31113..f005d55e41add3d1cd3c7fd506deb4c23b7d5005 100644 (file)
--- a/doc/userprog.texi
+++ b/doc/userprog.texi
@@ -674,6 +674,12 @@ as explicitly described below.
 
 Each process has an independent set of file descriptors.  File
 descriptors are not inherited by child processes.
 
 Each process has an independent set of file descriptors.  File
 descriptors are not inherited by child processes.

+
+When a single file is opened more than once, whether by a single
+process or different processes, each @code{open} returns a new file
+descriptor.  Different file descriptors for a single file are closed
+independently in separate calls to @code{close} and they do not share
+a file position.

 @end deftypefn
 
 @deftypefn {System Call} int filesize (int @var{fd})
 @end deftypefn
 
 @deftypefn {System Call} int filesize (int @var{fd})