From: Claudio Sacerdoti Coen Date: Fri, 21 Dec 2018 23:35:11 +0000 (+0100) Subject: HandleBox deprecated and no longer working X-Git-Tag: make_still_working~229^2~28 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e953541c8ace20b15836fda511a26044fce9a4e7;p=helm.git HandleBox deprecated and no longer working Replace with Box. It is used for natural deduction palette that is not very useful yet in the new Matita. --- diff --git a/matita/matita/matita.ui b/matita/matita/matita.ui index 3ea0c2dd9..1b567aef6 100644 --- a/matita/matita/matita.ui +++ b/matita/matita/matita.ui @@ -1767,10 +1767,9 @@ False 2 - + True False - top True