Admin/Linux/build
author wenzelm
Sun, 12 Mar 2017 17:59:03 +0100
changeset 65199 6bd7081f8319
parent 54313 da2e6282a4f5
child 71338 373dcdd363dc
permissions -rwxr-xr-x
clarified current_command: index refers to node content, negative index means first command;

#!/usr/bin/env bash

cc -static -m32 Isabelle.c -o Isabelle