| author | wenzelm |
| Tue, 24 Sep 2024 21:31:20 +0200 | |
| changeset 80946 | b76f64d7d493 |
| 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 |
} |