diff options
author | David Carlier <[email protected]> | 2019-07-04 09:19:07 +0000 |
---|---|---|
committer | David Carlier <[email protected]> | 2019-07-04 09:20:03 +0000 |
commit | 0533bf55effbcc3aba976ee223a569cecc628c2a (patch) | |
tree | aa3cb12ca3a7b29b4d7eac620b2d0c6bec2c36e5 /src/scripts | |
parent | 957b7395118e01169a3db130020b8f5e931ba499 (diff) |
Update the doc accordingly
Diffstat (limited to 'src/scripts')
-rwxr-xr-x | src/scripts/ci_build.py | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/src/scripts/ci_build.py b/src/scripts/ci_build.py index d8ac404e2..91d9d39a3 100755 --- a/src/scripts/ci_build.py +++ b/src/scripts/ci_build.py @@ -438,9 +438,6 @@ def main(args=None): if use_python3 and options.use_pylint3: cmds.append(['python3', '-m', 'pylint'] + pylint_flags + [py3_flags] + full_paths) - elif target == 'docker-android': - full_path = os.path.join(root_dir, 'src/scripts/docker-android.sh') - cmds.append(['sh', full_path]) else: config_flags, run_test_command, make_prefix = determine_flags( target, options.os, options.cpu, options.cc, |