Load prettify's lang-*.js extentions.

Kensuke Matsuzaki

2013-04-15 ed566a162c780faa0d6c84fac8fbbd3738586445

 src/main/distrib/data/gitblit.properties

@@ -76,6 +76,23 @@
# SINCE 1.1.0

git.submoduleUrlPatterns = .*?://github.com/(.*)



# Specify the interface for Git Daemon to bind it's service.

# You may specify an ip or an empty value to bind to all interfaces.

# Specifying localhost will result in Gitblit ONLY listening to requests to

# localhost.

#

# SINCE 1.3.0

# RESTART REQUIRED

git.daemonBindInterface = localhost



# port for serving the Git Daemon service.  <= 0 disables this service.

# On Unix/Linux systems, ports < 1024 require root permissions.

# Recommended value: 9418

#

# SINCE 1.3.0

# RESTART REQUIRED

git.daemonPort = 9418



# Allow push/pull over http/https with JGit servlet.

# If you do NOT want to allow Git clients to clone/push to Gitblit set this

# to false.  You might want to do this if you are only using ssh:// or git://.

@@ -145,6 +162,17 @@
#

# SINCE 1.1.0

git.defaultAuthorizationControl = NAMED



# The default incremental push tag prefix.  Tag prefix applied to a repository

# that has automatic push tags enabled and does not specify a custom tag prefix.

#

# If incremental push tags are enabled, the tips of each branch in the push will

# be tagged with an increasing revision integer.

#

# e.g. refs/tags/r2345 or refs/tags/rev_2345 
#

# SINCE 1.3.0

git.defaultIncrementalPushTagPrefix = r



# Enable JGit-based garbage collection. (!!EXPERIMENTAL!!)

#

@@ -723,9 +751,16 @@
web.forwardSlashCharacter = /



# Show other URLs on the summary page for accessing your git repositories

# Use spaces to separate urls. {0} is the token for the repository name.

# Use spaces to separate urls.

#

# {0} is the token for the repository name

# {1} is the token for the username

#

# The username is only practical if you have setup your other git serving

# solutions accounts to have the same username as the Gitblit account.

#

# e.g.

# web.otherUrls = ssh://localhost/git/{0} git://localhost/git/{0}

# web.otherUrls = ssh://localhost/git/{0} git://localhost/git/{0} https://{1}@localhost/r/{0}

#

# SPACE-DELIMITED

# SINCE 0.5.0

@@ -809,7 +844,7 @@
#

# SPACE-DELIMITED

# SINCE 0.5.0

web.prettyPrintExtensions = c cpp cs css frm groovy htm html java js php pl prefs properties py rb scala sh sql xml vb

web.prettyPrintExtensions = aea agc basic c cbm cl clj cpp cs css dart el erl erlang frm fs go groovy hs htm html java js latex lisp ll llvm lsp lua ml moxie mumps n nemerle pascal php pl prefs properties proto py r R rb rd Rd rkt s S scala scm sh Splus sql ss tcl tex vb vbs vhd vhdl wiki xml xq xquery yaml yml ymlapollo



# Registered extensions for markdown transformation

#

@@ -842,6 +877,16 @@
# RESTART REQUIRED

web.debugMode = false



# Force a default locale for all users, ignoring the browser's settings.

# An empty value allows Gitblit to use the translation preferred by the browser.

#

# Changing this value while the server is running will only affect new sessions.

#

# e.g. web.forceDefaultLocale = en

#

# SINCE 1.3.0

web.forceDefaultLocale = 


# Enable/disable global regex substitutions (i.e. shared across repositories)

#

# SINCE 0.5.0