delete files

arthuraa · Dec 26, 2011 · da30c73 · da30c73
1 parent bd04e93
commit da30c73
Show file tree

Hide file tree

Showing 13 changed files with 5 additions and 327 deletions.
diff --git a/.#commit.sh b/.#commit.sh
diff --git a/_build/check_term.cmi b/_build/check_term.cmi
diff --git a/_build/check_term.cmo b/_build/check_term.cmo
diff --git a/_build/check_term.inferred.cmi b/_build/check_term.inferred.cmi
diff --git a/_build/check_term.inferred.mli b/_build/check_term.inferred.mli
diff --git a/_build/check_term.inferred.mli.depends b/_build/check_term.inferred.mli.depends
diff --git a/_build/check_term.ml b/_build/check_term.ml
diff --git a/_build/check_term.ml.depends b/_build/check_term.ml.depends
diff --git a/_build/syntax.cmi b/_build/syntax.cmi
diff --git a/_build/syntax.cmo b/_build/syntax.cmo
diff --git a/_build/syntax.ml b/_build/syntax.ml
diff --git a/_build/syntax.ml.depends b/_build/syntax.ml.depends
diff --git a/commit.sh b/commit.sh
@@ -8,4 +8,8 @@ git push origin master
 
 # git remote add arthuraa https://github.com/arthuraa/cis670-project.git
 # git pull arthuraa master
-# git rm syntax.ml
+# git rm syntax.ml
+
+git add -u
+
+# It deletes all removed files and updates what was modified. Just doesn't add new files. It's better because if you have a file named "deleted.txt" it will also be removed.