[shell] #715938: support of script parameters (using standard '--' as arguments separator)
Arguments after bare "--" string will not be processed by the shell command
You can use it to pass extra arguments to your script and expect for
them in 'scriptargs' afterwards.
User's personnal information are modifiable using user's edit form. You can
access it through the dropdown-menu under the link on the top-right of the
window, labeled by your login. In this menu, click the "personal information"
link to go to this form.
Each user can as well customize the site appearance using the "user's
preferences" link in this menu. This will show you a form to configure which
boxes are displayed, in which order, etc...
.. image:: doc/images/userprefs