From 72e3b16bbd258e63f047392c973ba5e8f0a823c8 Mon Sep 17 00:00:00 2001
From: Sébastien Dailly <sebastien@chimrod.com>
Date: Tue, 1 Jun 2021 13:11:58 +0200
Subject: Added export button in editor

---
 editor/forms/delete_page.mli | 5 -----
 1 file changed, 5 deletions(-)
 delete mode 100755 editor/forms/delete_page.mli

(limited to 'editor/forms/delete_page.mli')

diff --git a/editor/forms/delete_page.mli b/editor/forms/delete_page.mli
deleted file mode 100755
index 0a3d9f9..0000000
--- a/editor/forms/delete_page.mli
+++ /dev/null
@@ -1,5 +0,0 @@
-type t = unit
-
-val create
-  : unit -> t Note.signal * Brr.El.t
-
-- 
cgit v1.2.3