Vadim Zeitlin d8da119ea1 Remove doxygen log file if it's empty in the helper script ... This allows to avoid having an untracked file in the repository, so it doesn't need to be ignored any longer, as it shouldn't exist after a successful run. Also output a warning if the log file is not empty, even though the full dump is only shown in the GitHub workflow file, as when running the script locally it may be more convenient to examine the log file in some other way.		2022-08-03 19:43:10 +02:00
..
ISSUE_TEMPLATE	Make the issue template even more prescriptive	2022-06-10 18:14:35 +02:00
workflows	Remove doxygen log file if it's empty in the helper script	2022-08-03 19:43:10 +02:00
CONTRIBUTING.md	Revert "Explain that GitHub PRs are temporarily disabled"	2022-01-12 23:42:18 +01:00