Coq

~jgross-h/coq/+git/coq:v8.0

  1. Git
  2. lp:~jgross-h/coq/+git/coq
  3. v8.0
Last commit made on 2022-08-27
Get this branch:
git clone -b v8.0 https://git.launchpad.net/~jgross-h/coq/+git/coq

Branch merges

Branch information

Name:
v8.0
Repository:
lp:~jgross-h/coq/+git/coq

Recent commits

f7777da... by Jason Gross

Merge PR #16349: [v8.0] Add support for `-h` and `--help` to configure

Reviewed-by: Alizter

b5abe0c... by Jason Gross

Add support for `-h` and `--help` to configure

d8b4083b2e865d6ab32e3aa33fa7eb50fa9c901f added a usage function without
adding support for calling it.

This will allow my scripts that configure multiple versions of Coq to
work more fluently.

6aecb9a... by notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>

Default CoqIDE modifiers for menu did not work (e.g. "d" was
activating the "d" template menu).

I backported svn revision 9349 from JMN which fixes the problem (even
though I don't know why the previous setting would have worked at some
early time around 2004, in 8.0, before 8.1 is released).

Log of r9349 was:

Changement des modifeurs par défaut dans CoqIDE (problème de
compatibilité entre architecture)

a4718ef... by herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>

Using explicitly-given lablgtkdir rather than +lablgtk2 for compiling
files in ide/ and ide/utils/.

This is a partial cherry-pick of 6b03510 and it should solve opam coq
issue 49 (https://github.com/coq/opam-coq-archive/issues/49).

ef2fe92... by Hugo Herbelin <email address hidden>

Being more robust on the location of lablgtk2 for coqmktop.ml.

45651d4... by Hugo Herbelin <email address hidden>

Ensuring that sed does not use a specific locale for characters >= 128,
so that it does not fail on files containing latin1 characters, as
e.g. g_omega.ml4.

05b9731... by Hugo Herbelin <email address hidden>

v8.0: Oops, fixing 647a7ac09269 which mistakenly committed generated files.

886a842... by Hugo Herbelin <email address hidden>

v8.0: Applying a configure patch by Catalin Hritcu.

- Fix use of ocaml in canonical_pwd and escape_var which, on his
  setting, produce extra warnings which disturb the configure (fix
  taken from branch 8.1).
- Fix detection of lablgtk2 via presence of gText.mli (search was done
  in a too specific path).

44d36a3... by Hugo Herbelin <email address hidden>

This branch was called V8-0-bugfix in the svn repository started by
Jean-Christophe Filliâtre. Renamed into v8.0 in December 2015 to fit
the naming scheme v8.X later adopted from v8.1, inserting this commit
on top of the branch at the time of its integration into the git
archive.

Note that the following 3 commits have been lost (though redone
afterwards in a different way):

------------------------------------------------------------------------
r16421 | herbelin | 2013-04-17 20:33:05 +0200 (mer. 17 avril 2013) | 1 ligne

File .gitignore for V8-0-bugfix.
------------------------------------------------------------------------
r15796 | herbelin | 2012-09-13 15:38:23 +0200 (jeu. 13 sept. 2012) | 1 ligne

V8-0-bugfix: backport trunk's revision 15603 for OCaml 4 support.
------------------------------------------------------------------------
r15794 | herbelin | 2012-09-13 14:41:12 +0200 (jeu. 13 sept. 2012) | 3 lignes

Updating 8.0 to be compiled with recent ocaml, camlp5, lablgtk.
Tested with ocaml 3.12.1, camlp5 6.02.3, lablgtk 2.14.2. Should still
work though with ocaml down to 3.07 (and possibly ocaml 3.06).

77f396f... by Hugo Herbelin <email address hidden>

Committing .gitignore.