equal
deleted
inserted
replaced
463 -v BOOL be verbose (default false) |
463 -v BOOL be verbose (default false) |
464 |
464 |
465 Build object-logic or run examples. Also creates browsing |
465 Build object-logic or run examples. Also creates browsing |
466 information (HTML etc.) according to settings. |
466 information (HTML etc.) according to settings. |
467 |
467 |
468 ISABELLE_USEDIR_OPTIONS= |
468 ISABELLE_USEDIR_OPTIONS=... |
469 |
469 |
470 ML_PLATFORM=x86-linux |
470 ML_PLATFORM=... |
471 ML_HOME=/usr/local/polyml-5.2.1/x86-linux |
471 ML_HOME=... |
472 ML_SYSTEM=polyml-5.2.1 |
472 ML_SYSTEM=... |
473 ML_OPTIONS=-H 500 |
473 ML_OPTIONS=... |
474 \end{ttbox} |
474 \end{ttbox} |
475 |
475 |
476 Note that the value of the @{setting_ref ISABELLE_USEDIR_OPTIONS} |
476 Note that the value of the @{setting_ref ISABELLE_USEDIR_OPTIONS} |
477 setting is implicitly prefixed to \emph{any} @{tool usedir} |
477 setting is implicitly prefixed to \emph{any} @{tool usedir} |
478 call. Since the @{verbatim IsaMakefile}s of all object-logics |
478 call. Since the @{verbatim IsaMakefile}s of all object-logics |