add omitted mockito.git in clean function (#277)

without cleaning mockito.git, the get_repos.sh may report error like "mv: cannot move ‘defects4j/project_repos/mockito.git’ to ‘./mockito.git’: Directory not empty" during execution.
rjust · Feb 8, 2020 · 502b915 · 502b915
1 parent 1980e05
commit 502b915
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/project_repos/get_repos.sh b/project_repos/get_repos.sh
@@ -12,6 +12,7 @@ clean() {
     commons-math.git \
     jfreechart \
     joda-time.git \
+    mockito.git \
     README 
 }