#
e5fd6926 |
|
28-Jan-2020 |
wenzelm <none@none> |
ignore generated dependency files (see 91d5a8255c98, fd5cd1daf6a9);
|
#
e681f157 |
|
12-Jun-2017 |
wenzelm <none@none> |
obsolete;
|
#
4fb0c7d9 |
|
06-May-2017 |
wenzelm <none@none> |
obsolete;
|
#
bf9a058c |
|
19-Dec-2016 |
wenzelm <none@none> |
basic support for VSCode Language Server protocol; minimal extension for VSCode editor;
|
#
f496032b |
|
14-Sep-2016 |
Lars Hupel <lars.hupel@mytum.de> |
ignore default output directory of 'build_stats' tool
|
#
cc08df05 |
|
31-May-2016 |
Lars Hupel <lars.hupel@mytum.de> |
ignore Maven build products
|
#
100bac12 |
|
05-Apr-2014 |
paulson <lp15@cam.ac.uk> |
ignore jedit mark files
|
#
7984a4b4 |
|
25-Jan-2014 |
wenzelm <none@none> |
reverted cb17feba74e0, avoid sweeping garbage under the carped (MaSh should not create .pyc files anymore, see also 778b2b8f4a35, 347f743e8336);
|
#
78308c3b |
|
25-Nov-2013 |
paulson <none@none> |
MaSH files should be ignored
|
#
48557385 |
|
22-Nov-2013 |
wenzelm <none@none> |
more .hgignore;
|
#
83b98387 |
|
28-Aug-2012 |
wenzelm <none@none> |
updated .hgignore to reflect to (almost) clean result of build_doc;
|
#
e2aece97 |
|
14-Aug-2012 |
wenzelm <none@none> |
ignore some administrative files on newer Mercurial versions as well;
|
#
d212f067 |
|
08-Jun-2011 |
wenzelm <none@none> |
simplified directory structure; recovered README.html; --HG-- rename : src/Tools/jEdit/dist-template/README.html => src/Tools/jEdit/README.html rename : src/Tools/jEdit/dist-template/properties/jedit.props => src/Tools/jEdit/src/jEdit.props rename : src/Tools/jEdit/dist-template/modes/isabelle-session.xml => src/Tools/jEdit/src/modes/isabelle-session.xml rename : src/Tools/jEdit/dist-template/modes/isabelle.xml => src/Tools/jEdit/src/modes/isabelle.xml
|
#
75d5d41b |
|
08-Jun-2011 |
wenzelm <none@none> |
removed obsolete Netbeans project setup;
|
#
5e0dedae |
|
01-May-2011 |
wenzelm <none@none> |
include static rail files for old manuals, to make standard make job independent of the "rail" executable;
|
#
9110f7b1 |
|
11-Jan-2010 |
wenzelm <none@none> |
ignore some src/Tools/jEdit stuff;
|
#
6c4832fd |
|
03-Jul-2009 |
wenzelm <none@none> |
more hgignore;
|
#
d3a119e3 |
|
16-Jun-2009 |
haftmann <none@none> |
ignore in-situ contrib symlinks
|
#
47a25ebb |
|
01-Dec-2008 |
wenzelm <none@none> |
ignore aux stuff in doc-src;
|
#
e148d36f |
|
29-Nov-2008 |
wenzelm <none@none> |
more .hgignore entries;
|
#
71c553e4 |
|
29-Nov-2008 |
wenzelm <none@none> |
basic setup of .hgignore;
|