Commit Graph

2 Commits

Author SHA1 Message Date
Arif Er 00f9ab19ac chore: update copyright headers to 2022
The script used to identify and update the change is added into the GitHub
workflows script directory. A workflow action can be created to trigger the
script to update the headers on the first of every new year. Possibly a task for
a consequent PR.
2022-06-03 17:32:20 +02:00
Maximilian Wolff 37c8669d36 [parinfer] Allow to disable auto-installation
instead a path to the library can be set manually.
See #14568
2021-05-17 21:24:54 +00:00