[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

Bug#950605: marked as done (Please, enable micro-C plugin)

Your message dated Tue, 07 Apr 2020 16:19:43 +0000
with message-id <E1jLqwx-000E0D-VB@fasolo.debian.org>
and subject line Bug#950605: fixed in why3 1.3.1-1
has caused the Debian Bug report #950605,
regarding Please, enable micro-C plugin
to be marked as done.

This means that you claim that the problem has been dealt with.
If this is not the case it is now your responsibility to reopen the
Bug report if necessary, and/or fix the problem forthwith.

(NB: If you are a system administrator and have no idea what this
message is talking about, this may indicate a serious mail system
misconfiguration somewhere. Please contact owner@bugs.debian.org
immediately.)


-- 
950605: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=950605
Debian Bug Tracking System
Contact owner@bugs.debian.org with problems
--- Begin Message --- 
Package: why3
Version: 1.2.1-2+b3
Severity: wishlist
Tags: upstream

Hi Ralf,

Upstream recently added a [micro-C] plugin that one can use [online],
but it’s not enabled in the Debian package.

  micro-C: https://gitlab.inria.fr/why3/why3/tree/master/plugins/microc
   online: http://why3.lri.fr/micro-C/

I realise it’s not actually available from the actual [source] used in
the Debian package, but don’t know why (that why I’ve also tagged this
bug “upstream”).

   source: https://gforge.inria.fr/frs/?group_id=2990

I’d very much like to use this plugin without the need to rely on a
webservice, so thanks in advance if you’re able to add such feature (and
yes, it’s already used in some courses ;).

Regards

David

Attachment: signature.asc
Description: PGP signature


--- End Message ---
--- Begin Message --- 
Source: why3
Source-Version: 1.3.1-1
Done: Ralf Treinen <treinen@debian.org>

We believe that the bug you reported is fixed in the latest version of
why3, which is due to be installed in the Debian FTP archive.

A summary of the changes between this version and the previous one is
attached.

Thank you for reporting the bug, which will now be closed.  If you
have further comments please address them to 950605@bugs.debian.org,
and the maintainer will reopen the bug report if appropriate.

Debian distribution maintenance software
pp.
Ralf Treinen <treinen@debian.org> (supplier of updated why3 package)

(This message was generated automatically at their request; if you
believe that there is a problem with it please contact the archive
administrators by mailing ftpmaster@ftp-master.debian.org)


-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA256

Format: 1.8
Date: Mon, 06 Apr 2020 09:35:10 +0200
Source: why3
Architecture: source
Version: 1.3.1-1
Distribution: unstable
Urgency: medium
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Changed-By: Ralf Treinen <treinen@debian.org>
Closes: 950605
Changes:
 why3 (1.3.1-1) unstable; urgency=medium
 .
   * New upstream version.
     This version contains the micro-C plugin (closes: #950605)
   * Drop patches fixed by this upstream version:
     - coq-8.10+11
     - 0002-Move-menhirLib-from-EXTOBJS-to-EXTLIBS
   * Refresh patch hardening-flags
   * Upstream switched the building of the documentation to sphinx:
     - added build-dependencies python3-sphinx, python3-sphinxcontrib.bibtex
     - dropped build-dependencies rubber, hevea, lmodern
     - why3-doc-pdf.docs: update path of manual.pdf
   * configuration: explicitly set --libdir
   * debian/rules: simplify by using override_dh_auto_build-{arch,indep}
   * Test why+coq: use /tmp when $ADT_ARTIFACTS is not set
   * why3-doc-html:
     - depend on libjs-{jquery,underscore}
     - use why3-doc-html.links to symlink these libraries, replacing the
       embedded copies
     - remove calls to the mathjax library from generated html code
Checksums-Sha1:
 e386b49cae5c733c787118babfc1afadbe21bbbb 2796 why3_1.3.1-1.dsc
 1e05ac170fedae6eca06354e6829c7257f96b2b1 5823991 why3_1.3.1.orig.tar.gz
 8d415299c1b50e1cdd3e31cb02dd37a2cc2ebf67 18028 why3_1.3.1-1.debian.tar.xz
 4911c262eefb89e05b0d8bb251d076aa6fae5298 15581 why3_1.3.1-1_source.buildinfo
Checksums-Sha256:
 3208db469ff0b6e93e4f55397a88a0e48c9c466b69c68ed1fa673fd233f71b22 2796 why3_1.3.1-1.dsc
 7b0d5e8f67aa3e964b44fe943cc7ea538a9ebef823713eda1b52fc0f0ccbec9b 5823991 why3_1.3.1.orig.tar.gz
 8d35f2375b052c182d0d258b92b87febfe75c0876cc01f6f881f04def64904c0 18028 why3_1.3.1-1.debian.tar.xz
 b40f4475214d78e47a4f92c59b83fa4cacda14614abb57e39dee97bc3260ab5b 15581 why3_1.3.1-1_source.buildinfo
Files:
 dd80574f0778e05151b555d915ee8630 2796 math optional why3_1.3.1-1.dsc
 0c2a5c869e9cd168e850adc7e7f872a8 5823991 math optional why3_1.3.1.orig.tar.gz
 c8cd309f3c63351c336b38e3a09f96ae 18028 math optional why3_1.3.1-1.debian.tar.xz
 8ef63323905006442fded26aa0832fd4 15581 math optional why3_1.3.1-1_source.buildinfo

-----BEGIN PGP SIGNATURE-----

iQIzBAEBCAAdFiEEAgVIKeEtDyqOZI5idFxHZtTKzf8FAl6MoTgACgkQdFxHZtTK
zf8YHQ//ar+O7IJBEnceN4LN84+IOIbw5lJmZKBAsOf8CME7XLEAMN9+okOWk+5b
2olLFzTFgaZ6Y/FfH3bfoJKi1+DiK7phLhVjrPefli7otWRsZU0qZRFDuLN6PpNV
q8WnGPqjkJv4tynxRAn/zvLaMUuRFgtIJI1ZtGZqJmRvVe1Oc7RUb3XqM4Cjr7yr
7ae+Z+sYep2Kcl3JaNTZRxtysFN5E+55mAdCP173nr+3HWQN37yYidN3E75VVl3l
wX+eIWdAfMd1UoKeWWQ5agiD/uKdRJXBVqhOnRmCyG/AOmNrDCxMsVgvFaTkySKj
s37IXWIE9BV0igMjs3wFBRLK1ipcKvAlbdOoBJpmLie+fhJovz50jmg5y5apOag+
L6uz0IHI1Oz3w6j+bFvYlcBCNnDCWnuNz8ulyhwODg/1a8Bn4ybljpt18avnzMrq
BggenJmx9akH8/FwQfU2YCQJKGolRrmlek40F6Y9S5pAItZWP5JuvR77/jWaOqQr
AN81qTLOjYV2EECp0YrHNUDnucPQBMrmJJ9luURncAKiYaX3iCTuoOOLR7vn32jD
shKui+EoouWhOl/tp/coo9oZpjiCQ6oAC5NQIAuuDAKvQwf6omkidYZdoY2xfgJQ
tAB9kVEY+L8Q1h5epM/vCjUjBn//SaiM5bao0knWc1wt/mifbjQ=
=iU6L
-----END PGP SIGNATURE-----

--- End Message ---
Reply to: