X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=doc%2Fuserprog.texi;h=b50dc364829edcc186491b875e68e1b4cd470a72;hb=2886710fa362574f5ce483ee9c8e573ab3afc000;hp=11d9875ce7beabe78e2ebb8e9079d7402bb31113;hpb=2ca95dc97c9dd591d0f71f1f4c411b3aeb82d690;p=pintos-anon

diff --git a/doc/userprog.texi b/doc/userprog.texi
index 11d9875..b50dc36 100644
--- a/doc/userprog.texi
+++ b/doc/userprog.texi
@@ -301,7 +301,7 @@ regardless of what user process or kernel thread is running.  In
 Pintos, kernel virtual memory is mapped one-to-one to physical
 memory, starting at @code{PHYS_BASE}.  That is, virtual address
 @code{PHYS_BASE} accesses physical
-address 0, virtual address @code{PHYS_BASE} + @t{0x1234} access
+address 0, virtual address @code{PHYS_BASE} + @t{0x1234} accesses
 physical address @t{0x1234}, and so on up to the size of the machine's
 physical memory.
 
@@ -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.
+
+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})