]> matita.cs.unibo.it Git - helm.git/commitdiff
projects / helm.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: f34f262)
Use lablgladecc -embed again
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 20 Dec 2018 22:12:36 +0000 (23:12 +0100)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 27 Sep 2019 13:45:21 +0000 (15:45 +0200)
matita/matita/Makefile patch | blob | history

diff --git a/matita/matita/Makefile b/matita/matita/Makefile
index 210920abe280e144ba9e1f864479bbb6f90f017d..35484ddf6bb323f693ff7b4f2446c3f840c3e3aa 100644 (file)
--- 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
Unnamed repository; edit this file 'description' to name the repository.