diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-10-19 14:45:42 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-10-19 14:45:42 -0700 |
| commit | ce8c429281fd1f7e4ac4d2b7133152c1d370df0c (patch) | |
| tree | 407400e728621cc9a5262e7112a93bd6acd0835a /src/mksubdirs | |
| parent | 7de0540252b62080ee9f98617f5718cb1ae08579 (diff) | |
Remove autotools build system. (#2639)
Diffstat (limited to 'src/mksubdirs')
| -rwxr-xr-x | src/mksubdirs | 16 |
1 files changed, 0 insertions, 16 deletions
diff --git a/src/mksubdirs b/src/mksubdirs deleted file mode 100755 index c96437caa..000000000 --- a/src/mksubdirs +++ /dev/null @@ -1,16 +0,0 @@ -#!/bin/bash -# -# The purpose of this file is to generate a .subdirs file in the build process. -# This file contains a file of relative paths to all of the theories relative -# to the current directory. Each Makefile.am should thus build its own .subdirs file. -# This assumes it is passed the equivalent of the $top_srcdir configure variable. -# -# Invocation: -# -# mksubdirs <top_srcdir> - -TOP_SRCDIR=$1 - -grep '^THEORIES = ' $TOP_SRCDIR/src/Makefile.theories | \ - cut -d' ' -f3- | tr ' ' "\n" | \ - xargs -I__D__ echo "$TOP_SRCDIR/src/theory/__D__/kinds" |