author | Fabian Huch <huch@in.tum.de> |
Wed, 06 Dec 2023 17:55:30 +0100 | |
changeset 79180 | 229f49204603 |
parent 73192 | e7437085e589 |
permissions | -rw-r--r-- |
54313
da2e6282a4f5
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff
changeset
|
1 |
/* Author: Makarius |
da2e6282a4f5
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff
changeset
|
2 |
|
da2e6282a4f5
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff
changeset
|
3 |
Main Isabelle application executable. |
da2e6282a4f5
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff
changeset
|
4 |
*/ |
da2e6282a4f5
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff
changeset
|
5 |
|
da2e6282a4f5
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff
changeset
|
6 |
#include <stdlib.h> |
da2e6282a4f5
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff
changeset
|
7 |
#include <stdio.h> |
da2e6282a4f5
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff
changeset
|
8 |
#include <string.h> |
da2e6282a4f5
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff
changeset
|
9 |
#include <sys/types.h> |
da2e6282a4f5
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff
changeset
|
10 |
#include <unistd.h> |
71338 | 11 |
#include <libgen.h> |
54313
da2e6282a4f5
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff
changeset
|
12 |
|
da2e6282a4f5
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff
changeset
|
13 |
|
da2e6282a4f5
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff
changeset
|
14 |
static void fail(const char *msg) |
da2e6282a4f5
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff
changeset
|
15 |
{ |
da2e6282a4f5
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff
changeset
|
16 |
fprintf(stderr, "%s\n", msg); |
da2e6282a4f5
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff
changeset
|
17 |
exit(2); |
da2e6282a4f5
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff
changeset
|
18 |
} |
da2e6282a4f5
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff
changeset
|
19 |
|
da2e6282a4f5
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff
changeset
|
20 |
|
da2e6282a4f5
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff
changeset
|
21 |
int main(int argc, char *argv[]) |
da2e6282a4f5
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff
changeset
|
22 |
{ |
71363 | 23 |
char **cmd_line = NULL, *cmd = NULL, *dcmd = NULL, *dname = NULL; |
54313
da2e6282a4f5
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff
changeset
|
24 |
int i = 0; |
da2e6282a4f5
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff
changeset
|
25 |
|
71363 | 26 |
dcmd = strdup(argv[0]); |
73190 | 27 |
if (dcmd == NULL) fail("Failed to allocate memory"); |
28 |
||
71363 | 29 |
dname = dirname(dcmd); |
71338 | 30 |
|
54314 | 31 |
cmd_line = malloc(sizeof(char *) * (argc + 1)); |
73189 | 32 |
if (cmd_line == NULL) fail("Failed to allocate memory"); |
54313
da2e6282a4f5
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff
changeset
|
33 |
|
71363 | 34 |
cmd = malloc(strlen(dname) + strlen("/lib/scripts/Isabelle_app") + 1); |
73189 | 35 |
if (cmd == NULL) fail("Failed to allocate memory"); |
71363 | 36 |
sprintf(cmd, "%s/lib/scripts/Isabelle_app", dname); |
54313
da2e6282a4f5
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff
changeset
|
37 |
|
73190 | 38 |
cmd_line[0] = cmd; |
54313
da2e6282a4f5
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff
changeset
|
39 |
for (i = 1; i < argc; i++) cmd_line[i] = argv[i]; |
54314 | 40 |
cmd_line[argc] = NULL; |
41 |
||
71338 | 42 |
execvp(cmd, cmd_line); |
43 |
fprintf(stderr, "Failed to execute application script \"%s\"\n", cmd); |
|
44 |
exit(2); |
|
54313
da2e6282a4f5
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff
changeset
|
45 |
} |