isabelle: Admin/Linux/Isabelle.c@a817e4335a31 (annotated)

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>
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file; wenzelm parents: diff changeset	11
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	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	14	{
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file; wenzelm parents: diff changeset	15	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	16	exit(2);
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file; wenzelm parents: diff changeset	17	}
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	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	21	{
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file; wenzelm parents: diff changeset	22	char **cmd_line = NULL;
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file; wenzelm parents: diff changeset	23	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	24
54314 8f7061babae4 proper NULL termination; wenzelm parents: 54313 diff changeset	25	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	26	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	27
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file; wenzelm parents: diff changeset	28	cmd_line[0] = malloc(strlen(argv[0]) + 5);
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file; wenzelm parents: diff changeset	29	if (cmd_line[0] == 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	30
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file; wenzelm parents: diff changeset	31	strcpy(cmd_line[0], argv[0]);
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file; wenzelm parents: diff changeset	32	strcat(cmd_line[0], ".run");
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file; wenzelm parents: diff changeset	33
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file; wenzelm parents: diff changeset	34	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	35
54314 8f7061babae4 proper NULL termination; wenzelm parents: 54313 diff changeset	36	cmd_line[argc] = NULL;
8f7061babae4 proper NULL termination; wenzelm parents: 54313 diff changeset	37
54313 da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file; wenzelm parents: diff changeset	38	execvp(cmd_line[0], cmd_line);
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file; wenzelm parents: diff changeset	39	fail("Failed to execute application script");
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file; wenzelm parents: diff changeset	40	}
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file; wenzelm parents: diff changeset	41

author	wenzelm
	Wed, 13 Jan 2016 21:44:26 +0100
changeset 62173	a817e4335a31
parent 54314	8f7061babae4
child 71338	373dcdd363dc
permissions	-rw-r--r--