| author | wenzelm | 
| Fri, 29 Nov 2024 00:25:03 +0100 | |
| changeset 81505 | 01f2936ec85e | 
| 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  | 
}  |