Skip to content

in "export problems" use the source file name by default for the json file name #44

Description

@kohlhase

I always have to enter the file name but it is always the file name of the source file.

Metadata

Metadata

Assignees

Labels

No labels
No labels

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions