.\" DO NOT MODIFY THIS FILE! It was generated by help2man 1.40.9. .TH MATITAC "1" "May 2012" "matitac 0.99.1" "User Commands" .SH NAME matitac \- Matita interative theorem prover - batch compiler .SH SYNOPSIS .B matitac [ \fIOPTION \fR... ] \fIFILE\fR .SH DESCRIPTION Matita batch compiler v0.99.1 .SH OPTIONS .HP \fB\-b\fR forces the baseuri of path .HP \fB\-I\fR Adds path to the list of searched paths for the include command .HP \fB\-conffile\fR Read configuration from filename .IP Default: debian/tmp/usr/share/matita//matita.conf.xml .HP \fB\-force\fR Force actions that would not be executed per default .HP \fB\-noprofile\fR Turns off profiling printings .HP \fB\-noinnertypes\fR Turns off inner types generation while publishing .HP \fB\-profile\-only\fR Activates only profiler with label matching the provided regex .HP \fB\-system\fR Act on the system library instead of the user one .IP WARNING: not for the casual user .HP \fB\-no\-default\-includes\fR Do not include the default searched paths for the include command .HP \fB\-execcomments\fR Execute the content of (** ... *) comments .HP \fB\-v\fR Verbose mode .HP \fB\-\-version\fR Prints version .HP \fB\-debug\fR Do not catch top\-level exception (useful for backtrace inspection) .HP \fB\-onepass\fR Enable only one disambiguation pass .TP \fB\-help\fR Display this list of options .TP \fB\-\-help\fR Display this list of options