diff options
Diffstat (limited to 'src/expr/mkkind')
| -rwxr-xr-x | src/expr/mkkind | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/expr/mkkind b/src/expr/mkkind index 294dc5d7e..d9c64b660 100755 --- a/src/expr/mkkind +++ b/src/expr/mkkind @@ -93,12 +93,12 @@ function nonatomic_operator { } function parameterized { - # parameterized K #children ["comment"] + # parameterized K1 K2 #children ["comment"] lineno=${BASH_LINENO[0]} check_theory_seen - register_kind "$1" "$2" "$3" + register_kind "$1" "$3" "$4" } function constant { |