diff options
Diffstat (limited to 'tlc-dist-server')
| -rwxr-xr-x | tlc-dist-server | 2 |
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 "$@" |