summaryrefslogtreecommitdiff
path: root/INSTALL.macosx
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2013-05-08 18:03:54 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2013-05-08 18:03:54 +0200
commitdb38bb4ad9aff74576d3b7f00028d48f0447d5bd (patch)
tree09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /INSTALL.macosx
parent6e34b272d789455a9be589e27ad3a998cf25496b (diff)
parent499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff)
Merge branch 'experimental/upstream' into upstream
Diffstat (limited to 'INSTALL.macosx')
-rw-r--r--INSTALL.macosx30
1 files changed, 0 insertions, 30 deletions
diff --git a/INSTALL.macosx b/INSTALL.macosx
deleted file mode 100644
index 43390616..00000000
--- a/INSTALL.macosx
+++ /dev/null
@@ -1,30 +0,0 @@
-INSTALLATION PROCEDURE FOR THE PRECOMPILED VERSION OF COQ SYSTEM UNDER MACOS X
-------------------------------------------------------------------------------
-
-Here comes an bundle version of CoqIdE that you can save anywhere you want on
-your disk.
-
-Its main limitation is that double clicking and drap&drop on the application
-icon of a .v file won't open the file ! You must use Menu/Ctrl-o to open a
-file. (GTK-OSX handles it but lablgtk don't as far as I know.)
-
-An other limitation is that Sortcut aren't MacOS like ! (The question is again
-how to make "" throw CaML.)
-
-Notice that "Compile" and "File"/"Export to" menu items should work (modulo
-(pdf)latex finding).
-
-if you want to use coqide from your terminal add
-
-alias coqide /YOUR_INSTALL_DIRECTORY/CoqIdEv8.3.app/Contents/MacOS/startcoqide
-
-at your ~/.profile. ("YOUR_INSTALL_DIRECTORY" is often "Applications"). Options
-such as -I/-R should work on this setting.
-
-You could also add
-/YOUR_INSTALL_DIRECTORY/CoqIdEv8.3.app/Contents/Resources/bin/ at your path to
-use coqtop/coq-tex/coq... from any terminal but CAUTION coqide of that directory
-won't work.
-
-
-See up-to-date informations on http://coq.inria.fr/download.