diff options
| -rw-r--r-- | otherlibs/dynlink/.cvsignore | 1 | ||||
| -rw-r--r-- | otherlibs/graph/.cvsignore | 1 | ||||
| -rw-r--r-- | otherlibs/num/.cvsignore | 2 | ||||
| -rw-r--r-- | otherlibs/str/regex-0.12/.cvsignore | 2 |
4 files changed, 6 insertions, 0 deletions
diff --git a/otherlibs/dynlink/.cvsignore b/otherlibs/dynlink/.cvsignore new file mode 100644 index 000000000..5ea9775e1 --- /dev/null +++ b/otherlibs/dynlink/.cvsignore @@ -0,0 +1 @@ +extract_crc diff --git a/otherlibs/graph/.cvsignore b/otherlibs/graph/.cvsignore new file mode 100644 index 000000000..6a060f267 --- /dev/null +++ b/otherlibs/graph/.cvsignore @@ -0,0 +1 @@ +graphics.ml diff --git a/otherlibs/num/.cvsignore b/otherlibs/num/.cvsignore new file mode 100644 index 000000000..683e2c569 --- /dev/null +++ b/otherlibs/num/.cvsignore @@ -0,0 +1,2 @@ +int_misc.ml +nat.ml diff --git a/otherlibs/str/regex-0.12/.cvsignore b/otherlibs/str/regex-0.12/.cvsignore new file mode 100644 index 000000000..7abff1dbe --- /dev/null +++ b/otherlibs/str/regex-0.12/.cvsignore @@ -0,0 +1,2 @@ +Makefile +config.status |