| author | wenzelm | 
| Thu, 08 Dec 2022 16:10:45 +0100 | |
| changeset 76604 | aaedcdfa2154 | 
| 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 | } |