no more Makefiles (switch to dune)

and moving unnecessary files out of the repo
backtracking · Sep 30, 2020 · 683356b · 683356b
1 parent b30b2b9
commit 683356b
Show file tree

Hide file tree

Showing 14 changed files with 12 additions and 1,396 deletions.
diff --git a/.gitignore b/.gitignore
@@ -1,32 +1,6 @@
-*.cm*
-*.annot
-*.o
-*.install
 .merlin
-/.depend
 /META
-/Makefile
-/autom4te.cache/
-/config.log
-/config.status
-/configure
-/graph.a
-/src/dot_lexer.ml
-/src/dot_parser.ml
-/src/dot_parser.mli
-/src/dot_parser.output
-/src/gml.ml
 /www/index.en.html
 /www/index.fr.html
 /www/version.prehtml
-/bin/
-/dgraph/dgraph.byte
-/dgraph/dgraph.opt
-/editor/editor.byte
-/editor/editor.opt
-/view_graph/viewgraph.byte
-/view_graph/viewgraph.opt
-/export
 _build
-graph.cmo
-doc
diff --git a/META.in b/META.in
diff --git a/Makefile b/Makefile
@@ -0,0 +1,12 @@
+
+all:
+	dune build
+
+test:
+	dune runtest
+
+doc:
+	dune build @doc
+
+clean:
+	dune clean