--- a/src/Tools/8bit/Makefile Mon Aug 12 16:28:15 1996 +0200
+++ b/src/Tools/8bit/Makefile Fri Aug 16 11:27:10 1996 +0200
@@ -38,7 +38,6 @@
# use LaTeX2e instead of LaTeX 2.09
# this flag is currently only sensible for perl script gen-isadoc
# set to empty string for LaTeX 2.09
-#USE2E='-2e'
USE2E='-2e'
# name of GNU make utility: `make' on linux box; `gmake' on solaris
@@ -53,7 +52,7 @@
#HYPER_R=113
HYPER_R=20
-CONFIGFIlES = config/Makefile config/key-table.inp config/conv-tables.inp
+CONFIGFILES = config/Makefile config/key-table.inp config/conv-tables.inp
#path stem to isabelle source, used by patcher
STEM = /usr/stud/oheimb/isabelle/
@@ -106,7 +105,7 @@
# ----------------------------------------------------
-all: $(CONFIGFIlES)\
+all: $(CONFIGFILES)\
bin/gen-isa2latex bin/gen-isaterm bin/gen-isavim bin/gen-isaaxe\
bin/gen-isa_gnu_emacs bin/gen-isa_xemacs bin/gen-isadoc\
configuration a2isa bin/isa2latex bin/a2isa\
@@ -133,11 +132,12 @@
####### configuration files and the Makefile
-$(CONFIGFIlES): Makefile
+$(CONFIGFILES): Makefile
@echo "configuring the configuration files"
@cd config;\
$(PERL) -pi \
-e "s#^USE2E\s*=.*#USE2E= $(USE2E)#g;" \
+ -e "s#^GMAKE\s*=.*#GMAKE= $(GMAKE)#g;" \
Makefile
@cd config;\
$(PERL) -pi \
@@ -156,6 +156,7 @@
@echo "configuring gen-isa2latex"
@cd perl/generators;\
$(PERL) -pi \
+ -e "s#GMAKE\s*=.*#GMAKE= \"$(GMAKE)\";#g;" \
-e "s&^#!.*&#!$(PERL)&g;" \
gen-isa2latex.pl
@rm -f bin/gen-isa2latex;\
--- a/src/Tools/8bit/config/Makefile Mon Aug 12 16:28:15 1996 +0200
+++ b/src/Tools/8bit/config/Makefile Fri Aug 16 11:27:10 1996 +0200
@@ -17,6 +17,7 @@
MAKEFLAGS='s'
USE2E= '-2e'
+GMAKE= gmake
FONTDOCFILES = ../doc/fontindex.dvi ../doc/keyindex.dvi ../doc/fkmatrix.dvi
# the dependent files
@@ -33,7 +34,7 @@
isa2latex:
@cd ../c-sources/isa2latex;\
- gmake
+ $(GMAKE)
../term/isaterm: key-table.inp
@echo "generating isaterm"
--- a/src/Tools/8bit/doc/Makefile Mon Aug 12 16:28:15 1996 +0200
+++ b/src/Tools/8bit/doc/Makefile Fri Aug 16 11:27:10 1996 +0200
@@ -10,7 +10,7 @@
# operate silently
MAKEFLAGS='s'
-LATEX=latex
+LATEX=latex2e
ISA2LATEX=isa2latex
CHECKOUT=co
Binary file src/Tools/8bit/doc/fkmatrix.dvi has changed
Binary file src/Tools/8bit/doc/fontindex.dvi has changed
Binary file src/Tools/8bit/doc/keyindex.dvi has changed
Binary file src/Tools/8bit/doc/manual.dvi has changed
--- a/src/Tools/8bit/doc/manual.itex Mon Aug 12 16:28:15 1996 +0200
+++ b/src/Tools/8bit/doc/manual.itex Fri Aug 16 11:27:10 1996 +0200
@@ -323,8 +323,8 @@
\subsection{Preparations}
-To use the 8bit package, you have to set respectively extend the content of the
-following environment variables:
+To use the 8bit package, you have to set (respectively extend) the content of
+the following environment variables and export them:
\begin{itemize}
\item \bt{ISABELLE8BIT}: set the directory of the Isabelle 8bit package,\\
--- a/src/Tools/8bit/perl/generators/gen-isa2latex.pl Mon Aug 12 16:28:15 1996 +0200
+++ b/src/Tools/8bit/perl/generators/gen-isa2latex.pl Fri Aug 16 11:27:10 1996 +0200
@@ -22,6 +22,7 @@
&initpwd;
$initial_dir = $ENV{'PWD'};
+$GMAKE= "gmake";
########################
# comand line processing
@@ -547,15 +548,15 @@
# execute Makefile
#
print "\nexecuting Makefile\n" if $do_debug;
-$status = system("gmake") ;
-if ($status) { die "\"gmake\" executed abnormally: $!\n";}
+$status = system($GMAKE) ;
+if ($status) { die "\"".$GMAKE."\" executed abnormally: $!\n";}
#$status = system("cp $conv_temp_dir/$conv_sub_dir/isa2latex $conv_source_dir");
# if ($status) { die "can't copy binary file to CONV_SOURCE_DIR: $!\n";}
#print "\nexecuting Makefile, cleaning up\n" if $do_debug;
-#$status = system("gmake clean");
-#if ($status) { die "\"gmake clean\" executed abnormally: $!\n";}
+#$status = system($GMAKE." clean");
+#if ($status) { die "\"".$GMAKE." clean\" executed abnormally: $!\n";}
#######################################################################
# process -s option
--- a/src/Tools/8bit/xemacs/isa_xemacs Mon Aug 12 16:28:15 1996 +0200
+++ b/src/Tools/8bit/xemacs/isa_xemacs Fri Aug 16 11:27:10 1996 +0200
@@ -28,7 +28,7 @@
#users init file ($HOME is added). This file is loaded after
#the init file $PREFIX.emacs
-INIT=.emacs_isa_xemacs
+INIT=.emacs_xemacs_isa
###############################################
# do not edit below