remote updates

2026-09-24 13:34:07 +00:00 · 2019-05-13 20:45:22 +02:00
parent 5bb963fa82
commit 60d67e5428
12 changed files with 88 additions and 25 deletions
@@ -0,0 +1,12 @@
+#!/usr/bin/env bash
+
+set -e
+
+cd "$(dirname "$0")/.."
+
+set -x
+
+script/ci-custom.py
+script/lint-python
+script/lint-cpp
+script/test