Move batch_configure script to tools subdir

astrada · May 11, 2019 · b96e13e · b96e13e
1 parent 1a6720c
commit b96e13e
Showing 1 changed file with 0 additions and 0 deletions.
diff --git a/batch_configure → tools/batch_configure b/batch_configure → tools/batch_configure