Script 'mail_helper' called by obssrc Hello community, here is the log from the commit of package coq for openSUSE:Factory checked in at 2023-06-29 17:28:52 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/coq (Old) and /work/SRC/openSUSE:Factory/.coq.new.13546 (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "coq" Thu Jun 29 17:28:52 2023 rev:22 rq:1095883 version:8.17.1 Changes: -------- --- /work/SRC/openSUSE:Factory/coq/coq.changes 2023-03-29 23:27:32.683567528 +0200 +++ /work/SRC/openSUSE:Factory/.coq.new.13546/coq.changes 2023-06-29 17:29:14.618581017 +0200 @@ -1,0 +2,14 @@ +Wed Jun 28 21:03:07 UTC 2023 - Aaron Puchert <aaronpuch...@alice-dsl.net> + +- Update to version 8.17.1. + * Fixed incorrect paths emitted by coqdep in some cases for META + files which prevented dune builds for plugins from working + correctly. + * Fixed shadowing of record fields in extraction to OCaml. + * Fixed an impossible-to-turn-off debug message "backtracking and + redoing byextend on ...". + * Fixed a major memory regression affecting MathComp 2. +- Classify desktop entry under Science instead of Education. +- Add screenshot URL to AppStream metadata. + +------------------------------------------------------------------- Old: ---- coq-8.17.0.tar.gz coq-refman-8.17.0.tar.xz coq-stdlib-8.17.0.tar.xz New: ---- coq-8.17.1.tar.gz coq-refman-8.17.1.tar.xz coq-stdlib-8.17.1.tar.xz ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ coq.spec ++++++ --- /var/tmp/diff_new_pack.f6ZGhK/_old 2023-06-29 17:29:16.534592240 +0200 +++ /var/tmp/diff_new_pack.f6ZGhK/_new 2023-06-29 17:29:16.538592264 +0200 @@ -26,7 +26,7 @@ %endif Name: coq -Version: 8.17.0 +Version: 8.17.1 Release: 0 Summary: Proof Assistant based on the Calculus of Inductive Constructions License: LGPL-2.1-only ++++++ coq-8.17.0.tar.gz -> coq-8.17.1.tar.gz ++++++ /work/SRC/openSUSE:Factory/coq/coq-8.17.0.tar.gz /work/SRC/openSUSE:Factory/.coq.new.13546/coq-8.17.1.tar.gz differ: char 12, line 1 ++++++ coq-refman-8.17.0.tar.xz -> coq-refman-8.17.1.tar.xz ++++++ /work/SRC/openSUSE:Factory/coq/coq-refman-8.17.0.tar.xz /work/SRC/openSUSE:Factory/.coq.new.13546/coq-refman-8.17.1.tar.xz differ: char 26, line 1 ++++++ coq-stdlib-8.17.0.tar.xz -> coq-stdlib-8.17.1.tar.xz ++++++ ++++++ fr.inria.coq.coqide.desktop ++++++ --- /var/tmp/diff_new_pack.f6ZGhK/_old 2023-06-29 17:29:17.762599433 +0200 +++ /var/tmp/diff_new_pack.f6ZGhK/_new 2023-06-29 17:29:17.766599457 +0200 @@ -4,7 +4,7 @@ Name=Coq IDE GenericName=Proof Assistant Comment=Proof Assistant based on the Calculus of Inductive Constructions -Categories=Education;Science;Math; +Categories=Science;Math; MimeType=text/x-coqsrc; Exec=coqide %F Icon=coq ++++++ fr.inria.coq.coqide.metainfo.xml ++++++ --- /var/tmp/diff_new_pack.f6ZGhK/_old 2023-06-29 17:29:17.778599527 +0200 +++ /var/tmp/diff_new_pack.f6ZGhK/_new 2023-06-29 17:29:17.782599551 +0200 @@ -40,7 +40,7 @@ <url type="homepage">https://coq.inria.fr/</url> <url type="bugtracker">https://github.com/coq/coq/issues</url> <url type="faq">https://github.com/coq/coq/wiki/The-Coq-FAQ</url> - <url type="help">https://coq.inria.fr/documentation</url> + <url type="help">https://coq.inria.fr/refman/practical-tools/coqide.html</url> <url type="donation">https://coq.inria.fr/consortium</url> <url type="vcs-browser">https://github.com/coq/coq</url> <url type="contribute">https://github.com/coq/coq/blob/master/CONTRIBUTING.md</url> @@ -56,6 +56,13 @@ <binary>coqide</binary> </provides> <project_license>LGPL-2.1-only</project_license> + <screenshots> + <screenshot type="default"> + <image type="source"> + https://coq.inria.fr/refman/_images/coqide.png + </image> + </screenshot> + </screenshots> <content_rating type="oars-1.1"/> </component>