author | wenzelm |
Mon, 23 Dec 2019 15:24:14 +0100 | |
changeset 71338 | 373dcdd363dc |
parent 54314 | 8f7061babae4 |
child 71363 | ce3409dfb18c |
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 |
{ |
71338 | 23 |
char **cmd_line = NULL, *cmd = NULL, *dcmd = NULL, *bcmd = NULL, *dname = NULL, *bname = 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 |
|
71338 | 26 |
dcmd = strdup(argv[0]); dname = dirname(dcmd); |
27 |
bcmd = strdup(argv[0]); bname = basename(bcmd); |
|
28 |
||
54314 | 29 |
cmd_line = malloc(sizeof(char *) * (argc + 1)); |
54313
da2e6282a4f5
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff
changeset
|
30 |
if (cmd_line == NULL) fail("Failed to allocate command line"); |
da2e6282a4f5
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff
changeset
|
31 |
|
71338 | 32 |
cmd = cmd_line[0]; |
33 |
cmd = malloc(strlen(dname) + strlen(bname) + strlen("/lib/scripts/.run") + 1); |
|
34 |
if (cmd == NULL) fail("Failed to allocate command name"); |
|
35 |
sprintf(cmd, "%s/lib/scripts/%s.run", dname, bname); |
|
54313
da2e6282a4f5
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff
changeset
|
36 |
|
da2e6282a4f5
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff
changeset
|
37 |
for (i = 1; i < argc; i++) cmd_line[i] = argv[i]; |
da2e6282a4f5
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff
changeset
|
38 |
|
54314 | 39 |
cmd_line[argc] = NULL; |
40 |
||
71338 | 41 |
execvp(cmd, cmd_line); |
42 |
fprintf(stderr, "Failed to execute application script \"%s\"\n", cmd); |
|
43 |
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
|
44 |
} |