aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.dockerignore36
1 files changed, 36 insertions, 0 deletions
diff --git a/.dockerignore b/.dockerignore
new file mode 100644
index 0000000..82209d9
--- /dev/null
+++ b/.dockerignore
@@ -0,0 +1,36 @@
+*
+# Begin files referenced by symlinks
+!README.md
+!AUTHORS
+!INSTALL.md
+!CeCILL-B
+# End files referenced by symlinks
+!*.opam
+!plugin
+!mathcomp
+
+**/*.d
+**/*.vo
+**/*.vio
+**/*.cm*
+**/*~
+**/*.glob
+**/*.aux
+**/*.a
+**/*.o
+**/*#
+**/Make*.coq
+**/Make*.coq.bak
+**/Make*.coq.conf
+mathcomp/ssreflect/ssreflect.ml4
+mathcomp/ssreflect/ssrmatching.ml4
+mathcomp/ssreflect/ssrmatching.mli
+# mathcomp/ssreflect/ssrmatching.v
+mathcomp/ssreflect/ssreflect_plugin.mllib
+mathcomp/ssreflect/ssreflect_plugin.mlpack
+mathcomp/ssreflect.ml4
+mathcomp/ssrmatching.ml4
+mathcomp/ssrmatching.mli
+mathcomp/ssrmatching.v
+mathcomp/ssreflect_plugin.mllib
+mathcomp/ssreflect_plugin.mlpack