Admin/Linux/build
author wenzelm
Tue, 26 Jan 2021 20:16:56 +0100
changeset 73191 6823dddf9cf1
parent 71338 373dcdd363dc
permissions -rwxr-xr-x
prefer dynamic linking: platform is always x86_64 (see 373dcdd363dc);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
54313
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
     2
73191
6823dddf9cf1 prefer dynamic linking: platform is always x86_64 (see 373dcdd363dc);
wenzelm
parents: 71338
diff changeset
     3
gcc -m64 -Wall Isabelle.c -o Isabelle