-the beginning of the command line. (Executing actions specified on the
-command line happens later.)
+the beginning of the command line. (Actions specified on the
+command line execute later.)
+
+@func{main} calls @func{random_init} to initialize the kernel random
+number generator. If the user specified @option{-rs} on the
+@command{pintos} command line, @func{parse_options} already did
+this, but calling it a second time is harmless.