[debbugs-tracker] bug#33437: closed ([PATCH] Add dune-build-system)

[GNU bug Tracking System]

Your message dated Tue, 18 Dec 2018 22:41:47 +0100
with message-id <address@hidden>
and subject line Re: [bug#33437] [PATCH] Add dune-build-system
has caused the debbugs.gnu.org bug report #33437,
regarding [PATCH] Add dune-build-system
to be marked as done.

(If you believe you have received this mail in error, please contact
address@hidden)


-- 
33437: http://debbugs.gnu.org/cgi/bugreport.cgi?bug=33437
GNU Bug Tracking System
Contact address@hidden with problems
> --- Begin Message ---
>
>
>
> Subject: 
>
> [PATCH] Add dune-build-system
>
>
>
>
> Date: 
>
> Mon, 19 Nov 2018 23:25:37 +0100
>
>
>
>
> Hi, here is a small patch series to add dune-build-system and convert a
> few packages to it.
>
>
>
> --- End Message ---
> --- Begin Message ---
>
>
>
> Subject: 
>
> Re: [bug#33437] [PATCH] Add dune-build-system
>
>
>
>
> Date: 
>
> Tue, 18 Dec 2018 22:41:47 +0100
>
>
>
>
> Le Mon, 19 Nov 2018 23:25:37 +0100,
> Julien Lepiller <address@hidden> a écrit :
>
> > Hi, here is a small patch series to add dune-build-system and convert
> > a few packages to it.
>
> pushed as 6e8986c8388e889eb74509999aea826fd440dcc4 -
> 34d5314e9c826b1f602f9aaa8d707ca594736aaf
>
>
> --- End Message ---