tool/bin/devtools_tool

#!/bin/bash -e

# This file serves as an alias for the 'dt' executable so that
# the legacy `dt` can be used.
# TODO(kenz): remove this file in ~6 months (April 2025).

echo Warning: devtools_tool has been replaced by dt. Please use dt instead.
dt $@