Commit 829ad579 authored by Andrei Paskevich's avatar Andrei Paskevich

merge .gitignore's + move apidoc/ to doc/apidoc/

parent 96fb8710
......@@ -2,11 +2,8 @@
*~
*.bak
*.o
*.svn
.*.swp
.why.conf
why.conf
.authors
*.cmx
*.cmo
*.cmi
......@@ -23,29 +20,12 @@ why.conf
/.depend.*
/semantic.cache
/TAGS
/depend.pdf
/output_why3
/output_coq
/apidoc
/dep.pdf
/distrib
/META
# /bench/
/bench/bench
/bench/programs/good/booleans/
/bench/programs/good/exceptions/
/bench/programs/good/for/
/bench/programs/good/list/
/bench/programs/good/see/
/bench/programs/good/set/
/bench/programs/good/recfun/
# /bench/plugins/
/bench/plugins/*.cm*
/bench/plugins/*.annot
/bench/plugins/config.log
# /bin/
/bin/why3.byte
/bin/why3.opt
......@@ -63,8 +43,6 @@ why.conf
/bin/why3bench.byte
/bin/why3bench.opt
/bin/why3bench
/bin/whytptp.byte
/bin/whytptp.opt
/bin/why3doc.byte
/bin/why3doc.opt
/bin/why3doc
......@@ -89,6 +67,7 @@ why.conf
/doc/manual.glo
/doc/manual.gls
/doc/manual.ist
/doc/manual.out
/doc/*.haux
/doc/*.pdf
/doc/manual.html
......@@ -97,108 +76,54 @@ why.conf
/doc/bnf
/doc/bnf.ml
/doc/*_bnf.tex
/doc/apidoc.tex
/doc/apidoc/*.html
# /share/
/share/*.cm*
/share/*.annot
/share/provers-detection-data.conf
# /share/emacs/
/share/emacs/semantic.cache
# /src/
/src/config.sh
/src/config.ml
/src/*.annot
/src/*.cm[aiox]
/src/*.cma
/src/*.cmxa
/src/*.[ao]
/src/*.a
# /src/coq-plugin/
/src/coq-plugin/*.cm*
/src/coq-plugin/*.annot
/src/coq-plugin/g_whytac.ml
# /src/config/
/src/config/*.cm*
/src/config/*.annot
# /src/core/
/src/core/*.cm*
/src/core/*.annot
# /src/driver/
/src/driver/*.annot
/src/driver/*.cm*
/src/driver/driver_parser.output
/src/driver/driver_lexer.ml
/src/driver/driver_parser.ml
/src/driver/driver_parser.mli
# /src/ide/
/src/ide/*.annot
/src/ide/*.cm*
# /src/bench/
/src/bench/*.annot
/src/bench/*.cm*
/src/driver/driver_parser.output
# /src/parser/
/src/parser/*.annot
/src/parser/*.cm*
/src/parser/parser.output
/src/parser/lexer.ml
/src/parser/parser.ml
/src/parser/parser.mli
/src/parser/parser.pre.ml
/src/parser/parser.pre.mli
# /src/printer/
/src/printer/*.cm*
/src/printer/*.annot
/src/printer/driver_lexer.ml
/src/printer/driver_parser.ml
/src/printer/driver_parser.mli
/src/printer/*.output
# /src/programs/
/src/programs/*.cm*
/src/programs/*.annot
/src/programs/pgm_parser.mli
/src/programs/pgm_parser.ml
/src/programs/pgm_lexer.ml
/src/programs/*.output
/src/parser/parser.pre.output
# /src/tptp2why/
/src/tptp2why/*.cm*
/src/tptp2why/*.annot
/src/tptp2why/tptpParser.mli
/src/tptp2why/tptpLexer.ml
/src/tptp2why/tptpParser.ml
/src/tptp2why/tptpParser.conflicts
/src/tptp2why/tptpParser.mli
/src/tptp2why/tptpParser.output
/src/tptp2why/tptpParser.automaton
/src/tptp2why/*.output
/src/tptp2why/tptpLexer.ml
# /src/transform/
/src/transform/*.cm*
/src/transform/*.annot
/src/tptp2why/tptpParser.conflicts
# /src/util/
/src/util/*.cm*
/src/util/*.annot
/src/util/dynlink_compat.ml
/src/util/rc.ml
# /src/why3doc
/src/why3doc/*.cm*
/src/why3doc/*.annot
# /tests/
/tests/test-jcf/
/tests/test-pgm-jcf/
/tests/test-claude/
# /examples/
/examples/programs/my_cosine/*.gappa
/examples/my_cosine/
/examples/scottish-private-club/
/examples/hello_proof/
......@@ -207,13 +132,16 @@ why.conf
/examples/programs/isqrt/
/examples/programs/course/
/examples/programs/wcet_hull/
/examples/programs/my_cosine/
/examples/programs/binary_search2/
/examples/programs/vacid_0_sparse_array/
/examples/programs/vacid_0_red_black_trees/
/examples/programs/vacid_0_red_black_trees_harness/
/examples/programs/next_digit_sum/
/examples/programs/vstte10_max_sum/
/examples/programs/vstte10_search_list/
/examples/programs/vstte10_aqueue/
/examples/programs/insertion_sort_list/
/examples/programs/mergesort_list/
/examples/programs/binary_search/
# theories
/theories/int/
# modules
/modules/stdlib/
/modules/string/
......@@ -293,8 +293,6 @@ install_local: bin/why3
# Whyml
########
PGMGENERATED =
PGM_FILES = pgm_ttree pgm_types pgm_pretty \
pgm_module pgm_wp pgm_env pgm_typing pgm_main
......@@ -328,16 +326,14 @@ bin/why3ml: bin/why3ml.@OCAMLBEST@
include .depend.programs
.depend.programs: $(PGMGENERATED)
.depend.programs:
$(OCAMLDEP) -slash -I src -I src/programs $(PGMML) $(PGMMLI) > $@
depend: .depend.programs
clean::
rm -f $(PGMGENERATED)
rm -f src/programs/*.cm[iox] src/programs/*.o
rm -f src/programs/*.annot src/programs/*~
rm -f src/programs/*.output src/programs/*.automaton
rm -f bin/why3ml.byte bin/why3ml.opt bin/why3ml
rm -f .depend.programs
......@@ -862,9 +858,12 @@ doc/bnf: doc/bnf.mll
$(OCAMLLEX) $<
$(OCAMLOPT) -o $@ doc/bnf.ml
doc: $(DOC)
DOC = api glossary ide intro library macros manpages \
manual starting syntax syntaxref version whyml
DOCTEX = $(addprefix doc/, $(addsuffix .tex, $(DOC)))
doc/manual.pdf: $(BNFTEX) doc/*.tex doc/manual.tex doc/version.tex
doc/manual.pdf: $(BNFTEX) $(DOCTEX)
cd doc; $(RUBBER) -d manual.tex
# doc/manual.html: doc/manual.tex doc/version.tex
......@@ -895,13 +894,13 @@ MODULESTODOC = util/util util/hashweak \
FILESTODOC = $(addsuffix .mli, $(addprefix src/, $(MODULESTODOC)))
apidoc: $(FILESTODOC)
mkdir -p apidoc
mkdir -p doc/apidoc
$(OCAMLDOC) -d apidoc -html -keep-code $(INCLUDES) \
$(LIBINCLUDES) -I src $(FILESTODOC)
# $(LIBML)
install_apidoc: apidoc
rsync -av apidoc/ marche@scm.gforge.inria.fr:/home/groups/why3/htdocs/apidoc/
rsync -av doc/apidoc/ marche@scm.gforge.inria.fr:/home/groups/why3/htdocs/apidoc/
doc/apidoc.tex: $(FILESTODOC)
$(OCAMLDOC) -o doc/apidoc.tex -latex -noheader -notrailer $(INCLUDES) \
......@@ -909,7 +908,7 @@ doc/apidoc.tex: $(FILESTODOC)
# $(LIBML)
clean::
rm -f apidoc/*
rm -f doc/apidoc/*
################
# generic rules
......
whybench.opt
whybench.byte
apidoc.tex
manual.out
next_digit_sum
vstte10_max_sum
vstte10_search_list
vstte10_aqueue
insertion_sort_list
mergesort_list
binary_search
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment