diff options
author | Makarand Dharmapurikar <makarandd@google.com> | 2017-04-19 10:30:07 -0700 |
---|---|---|
committer | Makarand Dharmapurikar <makarandd@google.com> | 2017-04-19 10:30:07 -0700 |
commit | 8f37606f607df0bed1fa9058491e4d658ebd4e1b (patch) | |
tree | d2f931ec7b2889e63f74c7f879ac15f980f7836e /WORKSPACE | |
parent | f583975f81e21dbf46dcef178a0aba71f1158ccc (diff) |
disable mongoose
Diffstat (limited to 'WORKSPACE')
-rw-r--r-- | WORKSPACE | 6 |
1 files changed, 0 insertions, 6 deletions
@@ -77,12 +77,6 @@ local_repository( path = "third_party/gflags", ) -git_repository( - name = "mongoose_repo", - commit = "4120a97945b41195a6223a600dae8e3b19bed19e", - remote = "https://github.com/makdharma/mongoose.git" -) - new_local_repository( name = "submodule_benchmark", path = "third_party/benchmark", |