From ad68bdd94d341369eb11bb1c541afc371d716af4 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre@roux01.fr>
Date: Sat, 5 Aug 2023 14:01:24 +0200
Subject: [PATCH] Forgotten probability.v in theories/Make (#1001)

This means probability.v is not compiled in any OPAM package for
instance.
---
 CHANGELOG_UNRELEASED.md | 4 ++++
 theories/Make           | 1 +
 2 files changed, 5 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index b43828ab4..74e2bafdb 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -3,6 +3,10 @@
 ## [Unreleased]
 
 ### Added
+
+- in `theories/Make`
+  + file `probability.v` (wasn't compiled in OPAM packages up to now)
+
 - in `measure.v`:
   + lemma `lebesgue_regularity_outer`
 
diff --git a/theories/Make b/theories/Make
index fffdba636..eb5a1f241 100644
--- a/theories/Make
+++ b/theories/Make
@@ -28,6 +28,7 @@ derive.v
 measure.v
 numfun.v
 lebesgue_integral.v
+probability.v
 summability.v
 signed.v
 itv.v