Merge pull request #14693 from overleaf/unknown-document-environment

Set EnvName as optional in Environment definition

GitOrigin-RevId: feb048199737108734df45fd4a057d932a6bf785
This commit is contained in:
Alf Eaton 2023-09-11 10:53:22 +01:00 committed by Copybot
parent 42f288dc28
commit 7b8a8974dc

View file

@ -613,9 +613,9 @@ EnvNameGroup<name> {
}
Environment[@isGroup="$Environment"] {
BeginEnv<EnvName>
BeginEnv<EnvName?>
Content<Text>
EndEnv<EnvName>
EndEnv<EnvName?>
}
Group<GroupContent> {