Move extras/ into a git submodule.

2 files changed, 0 insertions, 14 deletions

diff --git a/extras b/extras
new file mode 160000
+Subproject 13dfbba8d21b843cc3bb871ed06088ca72cde8c
diff --git a/extras/dump_sections b/extras/dump_sections
deleted file mode 100755
index 362318f30..000000000
--- a/extras/dump_sections
+++ /dev/null
@@ -1,14 +0,0 @@
-#!/bin/bash
-# This wraps dump_sections.py so that other python scripts can import the
-# functions. If dump_sections.py was instead called dump_sections, then other
-# python source code would be unable to use the functions via import
-# statements.
-
-# figure out the path to this script
-cwd="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
-
-# construct the path to dump_sections.py
-secpath=$cwd/dump_sections.py
-
-# run dump_sections.py
-$secpath $1