Skip to content

Commit

Permalink
Merge pull request kind2-mc#1103 from erooke/doc-fix
Browse files Browse the repository at this point in the history
docs: fix references to lustre_main in docs
  • Loading branch information
daniel-larraz authored Oct 3, 2024
2 parents ea7eb97 + 03bd512 commit 59c9a53
Show file tree
Hide file tree
Showing 3 changed files with 4 additions and 4 deletions.
2 changes: 1 addition & 1 deletion doc/usr/source/2_input/1_lustre.rst
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,7 @@ You can also specify the main node in the command line arguments, with

.. code-block:: none
kind2 --lustre_main <node_name> ...
kind2 --lus_main <node_name> ...
Main nodes specified by the command line option override main nodes annotated in the source code. If any main nodes exist then only main nodes are analyzed (top nodes are not).

Expand Down
2 changes: 1 addition & 1 deletion doc/usr/source/9_other/8_interpreter.rst
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ Interpreter
The interpreter is a special mode where Kind 2 reads input values from
a file and prints the computed values for the output and local variables
of a node at each step. If the Lustre file contains two or more top nodes,
a single node must be selected with either the command-line option :code:`--lustre_main <node_name>` or
a single node must be selected with either the command-line option :code:`--lus_main <node_name>` or
a single :code:`--%MAIN` annotation in the Lustre file.

To use the interpreter, run:
Expand Down
4 changes: 2 additions & 2 deletions src/lustre/lustreInput.mli
Original file line number Diff line number Diff line change
Expand Up @@ -41,13 +41,13 @@
The main node is chosen to be, in order of precedence:
- the node with the name given by the [--lustre_main] command-line
- the node with the name given by the [--lus_main] command-line
option,
- the node with the annotation [--%MAIN], or
- the last node in the input.
An exception [Invalid_argument] is raised if the node given by
[--lustre_main] is not found, there are two nodes with a [--%MAIN]
[--lus_main] is not found, there are two nodes with a [--%MAIN]
annotation, or the input contains no nodes.
In particular, the output of the entry point {!LustreParser.main}
Expand Down

0 comments on commit 59c9a53

Please sign in to comment.