diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-10-15 14:43:33 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-10-15 14:43:33 -0700 |
| commit | 80b14c0965678fb91467de287b00a9a1d8a39be5 (patch) | |
| tree | 34d3da127ab61bc9adfff4b0298dc4f4c153d1be /src/expr/kind_template.h | |
| parent | c5eb0c1900e8cf12a18d15d8b1c0660c626bf137 (diff) | |
Fix line numbers in templates (#3391)
This commit updates the line numbers in templates to address warnings
due to wrong line numbers.
Diffstat (limited to 'src/expr/kind_template.h')
| -rw-r--r-- | src/expr/kind_template.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h index 0168363d4..da8e48a6f 100644 --- a/src/expr/kind_template.h +++ b/src/expr/kind_template.h @@ -68,7 +68,7 @@ struct KindHashFunction { enum CVC4_PUBLIC TypeConstant { ${type_constant_list} -#line 71 "${template}" +#line 72 "${template}" LAST_TYPE }; /* enum TypeConstant */ |