diff options
Diffstat (limited to 'Makefile.dev')
| -rw-r--r-- | Makefile.dev | 40 |
1 files changed, 4 insertions, 36 deletions
diff --git a/Makefile.dev b/Makefile.dev index 0461fe0728..9659f602d7 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -20,10 +20,7 @@ DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo devel: printers -printers: $(CORECMA) $(DEBUGPRINTERS) dev/camlp5.dbg - -dev/camlp5.dbg: - echo "load_printer gramlib.cma" > $@ +printers: $(CORECMA) $(DEBUGPRINTERS) ############ # revision @@ -34,33 +31,8 @@ dev/camlp5.dbg: revision: $(SHOW)'CHECK revision' $(HIDE)rm -f revision.new -ifeq ($(CHECKEDOUT),svn) - $(HIDE)set -e; \ - if test -x "`which svn`"; then \ - export LC_ALL=C;\ - svn info . | sed -ne '/URL/s/.*\/\([^\/]\{1,\}\)/\1/p' > revision.new; \ - svn info . | sed -ne '/Revision/s/Revision: \([0-9]\{1,\}\)/\1/p'>> revision.new; \ - fi -endif -ifeq ($(CHECKEDOUT),gnuarch) $(HIDE)set -e; \ - if test -x "`which tla`"; then \ - LANG=C; export LANG; \ - tla tree-version > revision.new ; \ - tla tree-revision | sed -ne 's|.*--||p' >> revision.new ; \ - fi -endif -ifeq ($(CHECKEDOUT),git) - $(HIDE)set -e; \ - if test -x "`which git`"; then \ - LANG=C; export LANG; \ - GIT_BRANCH=$$(git branch -a | sed -ne '/^\* /s/^\* \(.*\)/\1/p'); \ - GIT_HOST=$$(hostname); \ - GIT_PATH=$$(pwd); \ - (echo "$${GIT_HOST}:$${GIT_PATH},$${GIT_BRANCH}") > revision.new; \ - (echo "$$(git log -1 --pretty='format:%H')") >> revision.new; \ - fi -endif + ./dev/tools/make_git_revision.sh > revision.new $(HIDE)set -e; \ if test -e revision.new; then \ if test -e revision; then \ @@ -169,12 +141,9 @@ noreal: unicode logic arith bool zarith qarith lists sets fsets \ ################ OMEGAVO:=$(filter plugins/omega/%, $(PLUGINSVO)) -ROMEGAVO:=$(filter plugins/romega/%, $(PLUGINSVO)) MICROMEGAVO:=$(filter plugins/micromega/%, $(PLUGINSVO)) -QUOTEVO:=$(filter plugins/quote/%, $(PLUGINSVO)) RINGVO:=$(filter plugins/setoid_ring/%, $(PLUGINSVO)) NSATZVO:=$(filter plugins/nsatz/%, $(PLUGINSVO)) -FOURIERVO:=$(filter plugins/fourier/%, $(PLUGINSVO)) FUNINDVO:=$(filter plugins/funind/%, $(PLUGINSVO)) BTAUTOVO:=$(filter plugins/btauto/%, $(PLUGINSVO)) RTAUTOVO:=$(filter plugins/rtauto/%, $(PLUGINSVO)) @@ -183,12 +152,11 @@ CCVO:= DERIVEVO:=$(filter plugins/derive/%, $(PLUGINSVO)) LTACVO:=$(filter plugins/ltac/%, $(PLUGINSVO)) -omega: $(OMEGAVO) $(OMEGACMO) $(ROMEGAVO) $(ROMEGACMO) +omega: $(OMEGAVO) $(OMEGACMO) micromega: $(MICROMEGAVO) $(MICROMEGACMO) $(CSDPCERT) setoid_ring: $(RINGVO) $(RINGCMO) nsatz: $(NSATZVO) $(NSATZCMO) extraction: $(EXTRACTIONCMO) $(EXTRACTIONVO) -fourier: $(FOURIERVO) $(FOURIERCMO) funind: $(FUNINDCMO) $(FUNINDVO) cc: $(CCVO) $(CCCMO) rtauto: $(RTAUTOVO) $(RTAUTOCMO) @@ -196,7 +164,7 @@ btauto: $(BTAUTOVO) $(BTAUTOCMO) ltac: $(LTACVO) $(LTACCMO) .PHONY: omega micromega setoid_ring nsatz extraction -.PHONY: fourier funind cc rtauto btauto ltac +.PHONY: funind cc rtauto btauto ltac # For emacs: # Local Variables: |