From 9029c61539cf13aa6a6921510a7c2e568225f328 Mon Sep 17 00:00:00 2001 From: Jeremie Dimino Date: Sun, 1 Jul 2018 21:57:17 +0100 Subject: [PATCH] Update changelog Signed-off-by: Jeremie Dimino --- CHANGES.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGES.md b/CHANGES.md index f418619e..c2fceb22 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -93,7 +93,7 @@ next - Make `dev` the default build profile (#920, @diml) -- Version `dune-workspace` and `~/.config/dune/config` files (#..., @diml) +- Version `dune-workspace` and `~/.config/dune/config` files (#932, @diml) - Add the ability to build an alias non-recursively from the command line by writing `@@alias` (#926, @diml)