diff options
| author | Philipp Gesang <phg42.2a@gmail.com> | 2014-05-16 23:11:33 +0200 |
|---|---|---|
| committer | Philipp Gesang <phg42.2a@gmail.com> | 2014-05-16 23:11:33 +0200 |
| commit | 9920c7babc22260bfb154281db531a0250744d8d (patch) | |
| tree | f9d07c6d3037e486644f388de5bdd176958ab673 | |
| parent | 8f140a216eb5a75dea48a9ff67dbead66d0210b5 (diff) | |
| download | context-mirror-bot-9920c7babc22260bfb154281db531a0250744d8d.tar.gz | |
remove wrapper for git-add
| -rw-r--r-- | context_mirror_bot.ml | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/context_mirror_bot.ml b/context_mirror_bot.ml index ecebed5..a080dea 100644 --- a/context_mirror_bot.ml +++ b/context_mirror_bot.ml @@ -366,13 +366,6 @@ end = struct | Some _ -> true | None -> false - let add timestamp = - exec_commands [ "git add ."; - "git add --update"; - Printf.sprintf - "git commit --message=\"%s\"" - (format_time timestamp) ] - let gc () = msg ~lev:1 "Running git garbage collector."; ignore (list_of_pipe "git gc") |