From 2b9f8373fa1d5eaecb3998a8ba934b66d852bf10 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 20 Dec 2018 23:12:36 +0100 Subject: [PATCH] Use lablgladecc -embed again --- matita/matita/Makefile | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/matita/matita/Makefile b/matita/matita/Makefile index 210920abe..35484ddf6 100644 --- a/matita/matita/Makefile +++ b/matita/matita/Makefile @@ -143,8 +143,7 @@ matitaclean.opt: matitac.opt $(H)test -f $@ || ln -s $< $@ matitaGeneratedGui.ml: matita.ui - #$(H)$(LABLGLADECC) -embed $< > matitaGeneratedGui.ml - $(H)$(LABLGLADECC) $< > matitaGeneratedGui.ml + $(H)$(LABLGLADECC) -embed $< > matitaGeneratedGui.ml .PHONY: clean -- 2.39.2