]> matita.cs.unibo.it Git - helm.git/commitdiff
enable building with ocaml 3.08.x
authorStefano Zacchiroli <zack@upsilon.cc>
Thu, 12 Jan 2006 10:56:18 +0000 (10:56 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Thu, 12 Jan 2006 10:56:18 +0000 (10:56 +0000)
- do not build the GUI (which requires lablgtksourceview)
- do not append -for-pack
- checkout from the tests branch

helm/matita/Makefile.in
helm/matita/configure.ac
helm/matita/scripts/crontab.sh
helm/matita/scripts/profile_svn.sh
helm/ocaml/paramodulation/Makefile

index 0614bda3d44a067a310de7dcaca1e9387c58f248..d498e37a102395521c3ec4e77a6147f2cbba8b18 100644 (file)
@@ -72,7 +72,7 @@ MAKECMOS = \
        buildTimeConf.cmo       \
        matitamakeLib.cmo       \
        $(NULL)
-PROGRAMS_BYTE = matita matitac cicbrowser matitadep matitaclean matitamake dump_moo
+PROGRAMS_BYTE = matitac matitadep matitaclean matitamake
 PROGRAMS = $(PROGRAMS_BYTE) matitatop
 PROGRAMS_OPT = $(patsubst %,%.opt,$(PROGRAMS_BYTE))
 
index 1075d605d4d025496621b4bf47e8cee5f61315fb..f448eb76751852b64b10abcb7479ec7752034e4f 100644 (file)
@@ -54,7 +54,6 @@ FINDLIB_REQUIRES="\
 $FINDLIB_CREQUIRES \
 lablgtk2.glade \
 lablgtkmathview \
-lablgtksourceview \
 helm-xmldiff \
 helm-paramodulation \
 "
index 5ad50de5ee47ea77bb1a997c1fb067a5752ba4e8..3f5dfb97811647f3e0b942d1394674bbef2fa6cd 100644 (file)
@@ -3,7 +3,7 @@ TODAY=`date +%Y%m%d`
 YESTERDAY=`date -d yesterday +%Y%m%d`
 TMPDIRNAME=$HOME/__${TODAY}_crontab
 TMPDIRNAMEOLD=$HOME/__${YESTERDAY}_crontab
-SVNROOT="svn+ssh://mowgli.cs.unibo.it/local/svn/helm/trunk/"
+SVNROOT="svn+ssh://mowgli.cs.unibo.it/local/svn/helm/branches/tests/"
 SHELLTIME2CENTSPHP=scripts/shell_time2cents.php
 SHELLADDERPHP=scripts/shell_adder.php
 COMMONPHP=scripts/public_html/common.php
index eca457ecc89f129980b2ab700da184c203c7d09e..4642b353898eae59f8f2291b4ae182ad4a0d2836 100755 (executable)
@@ -1,7 +1,7 @@
 #!/bin/bash
 MARK=`date +%Y%m%d%H%M`
 TMPDIRNAME=__${MARK}_compilation
-SVNROOT="svn+ssh://mowgli.cs.unibo.it/local/svn/helm/trunk/"
+SVNROOT="svn+ssh://mowgli.cs.unibo.it/local/svn/helm/branches/tests/"
 
 function testit {
   LOGTOOPT=/dev/null
index 35b650ea71f8905d41e425783375a2bf0c42590e..900aca6b8996a2a284c2b60812723a5a8e8e1fd9 100644 (file)
@@ -14,12 +14,9 @@ include ../Makefile.common
 paramodulation.cmo: $(IMPLEMENTATION_FILES:%.ml=%.cmo)
        $(OCAMLC) -pack -o $@ $(IMPLEMENTATION_FILES:%.ml=%.cmo)
 
-paramodulation.cmx: OCAMLOPTIONS=-package "$(REQUIRES)" -predicates "$(PREDICATES)" -thread
 paramodulation.cmx: $(IMPLEMENTATION_FILES:%.ml=%.cmx)
        $(OCAMLOPT) -pack -o $@ $(IMPLEMENTATION_FILES:%.ml=%.cmx)
 
-OCAMLOPTIONS+=-for-pack Paramodulation
-
 $(ARCHIVE): paramodulation.cmo $(LIBRARIES)
        $(OCAMLC) $(OCAMLARCHIVEOPTIONS) -a -o $@ \
                paramodulation.cmo