Skip to content

Commit 1be9127

Browse files
committed
Ignore newly introduced TLC code.
Introduce in tlaplus/tlaplus Git commit 96056d942b70656e7f88349e2f1fa38514c48783 tlaplus/tlaplus@96056d9 tlaplus/tlaplus#1183 [Feature][TLC] Signed-off-by: Markus Alexander Kuppe <[email protected]>
1 parent b30c91c commit 1be9127

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

src/parsers/tlcCodes.ts

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -256,6 +256,7 @@ export const TLC_COVERAGE_INIT = registerCode(2773, TlcCodeType.Info);
256256
export const TLC_COVERAGE_PROPERTY = registerCode(2774, TlcCodeType.Ignore);
257257
export const TLC_COVERAGE_END_OVERHEAD = registerCode(2777, TlcCodeType.Ignore);
258258
export const TLC_COVERAGE_CONSTRAINT = registerCode(2778, TlcCodeType.Ignore);
259+
export const TLC_COVERAGE_VAR = registerCode(2779, TlcCodeType.Ignore);
259260

260261
// config file errors
261262
export const TLC_CONFIG_VALUE_NOT_ASSIGNED_TO_CONSTANT_PARAM = registerCode(2222, TlcCodeType.Error);

0 commit comments

Comments
 (0)