#!/bin/bash set -e username=$1 shift curl http://localhost:8001 -d "op=set_input&username=user_manager&element_type=V&value=\"$username\"" -s -S >> /dev/null python interface/HUTN/hutn_compiler/linker.py $username "$@"
