summarylogtreecommitdiffstats
path: root/tlc-dist-server
diff options
context:
space:
mode:
authorDavid Barri2019-03-17 19:31:51 +1100
committerDavid Barri2019-03-17 19:31:51 +1100
commitf9d6a8d39646d547239fb4f508ff9170283602f0 (patch)
treed0fc8a48214ab62493438d0ad10538ba48076406 /tlc-dist-server
parentf1dbd634856c2391c2123ce1f35f9443ee9d9e8f (diff)
downloadaur-f9d6a8d39646d547239fb4f508ff9170283602f0.tar.gz
Add tlc-dist-*
Diffstat (limited to 'tlc-dist-server')
-rwxr-xr-xtlc-dist-server2
1 files changed, 2 insertions, 0 deletions
diff --git a/tlc-dist-server b/tlc-dist-server
new file mode 100755
index 000000000000..0735edec1958
--- /dev/null
+++ b/tlc-dist-server
@@ -0,0 +1,2 @@
+#!/bin/sh
+exec tla-tools tlc2.tool.distributed.TLCServer "$@"