*vl-server-help*
Value:
"
vl server: Runs the VL Server (which supports the Module Browser).
Usage: vl server [OPTIONS]
Options:
-h,--help Show a brief usage message and exit.
--readme Show a more elaborate README and exit.
-m,--mem=GB Default: 6 GB. How much memory to try to
use. Raising this may improve performance by
avoiding garbage collection. To avoid
swapping, keep this below (physical_memory -
2 GB).
-p,--port=ARG Default: 9999. What port to run on.
-r,--root=ARG Default: \"./translations\". Where to find
translations. See the --readme to understand
this.
--public=ARG Default:
\"/var/lib/jenkins/workspace/acl2-master/books/centaur/vl/server/public\".
Where to find the supporting 'public'
directory from the module browser's code.
You should be able to ignore this unless
you're deploying the module browser to a
different directory.
"
